ofLogicRat
plain-language theorem explainer
This definition embeds a recovered rational into the recovered complex numbers by first mapping it through the recovered reals. Foundation developers cite it when lifting rational data into the complex carrier for transport arguments. The implementation is a direct composition of the real embedding followed by the real-to-complex embedding with zero imaginary part.
Claim. Let $q$ be a recovered rational. Then ofLogicRat$(q)$ is the recovered complex number whose real part equals the recovered-real embedding of $q$ and whose imaginary part is zero.
background
The module ComplexFromLogic builds complex numbers over the recovered real line without redeveloping analysis. LogicComplex is the structure whose fields are a pair of recovered reals (real and imaginary parts). The local convention supplies only the carrier and its equivalence to Mathlib ℂ, leaving analytic notions to later modules that invoke the transport explicitly.
proof idea
One-line wrapper that applies ofLogicReal to the result of RealsFromLogic.ofLogicRat on the input rational.
why it matters
It supplies the rational-to-complex map used by the downstream theorem toComplex_ofLogicRat, which shows that transport recovers the standard embedding of the rational into ℂ. The definition therefore closes one link in the foundation chain that equates recovered carriers with standard mathematics, enabling uniform use of rationals inside complex expressions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.