toComplex
plain-language theorem explainer
The definition embeds a LogicComplex, formed as a pair of recovered reals, into Mathlib's complex numbers by applying the real transport to each component. Researchers building carrier equivalences between logic-derived structures and standard analysis cite this map. It is realized directly as a pair constructor that invokes toReal on the real and imaginary parts.
Claim. The map sending a complex number $z$ built from recovered reals to the standard complex number in $ℂ$ whose real part is toReal of the recovered real component and whose imaginary part is toReal of the recovered imaginary component.
background
LogicComplex is the structure whose fields are two LogicReal values, one for the real part and one for the imaginary part. The toReal function from RealsFromLogic sends a recovered real to a standard real via CompareReals.compareEquiv. The module constructs the carrier for complex numbers over recovered reals and proves its equivalence with Mathlib's $ℂ$, so that later analytic work can invoke standard complex operations through the transport.
proof idea
One-line wrapper that applies toReal to the re and im fields of the LogicComplex structure and packages the results as a Mathlib complex number via the pair constructor.
why it matters
This supplies the forward direction of equivComplex, which is used to prove logicComplex_recovered_from_mathlib and the equality transfer eq_iff_toComplex_eq. It completes the transport layer in the foundation sequence from recovered reals to recovered complexes, allowing downstream theorems on addition and division to reduce to Mathlib arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.