toComplex_fromComplex
plain-language theorem explainer
The round-trip through the recovered LogicComplex carrier returns any Mathlib complex number unchanged. Equivalence builders and downstream simplifications cite this to confirm faithful transport on the complex side. The proof is a one-line wrapper applying complex extensionality followed by simplification with the component definitions and the real round-trip theorem.
Claim. For every $z : ℂ$, toComplex(fromComplex $z$) = $z$, where fromComplex sends $z$ to the LogicComplex pair (fromReal(Re $z$), fromReal(Im $z$)) and toComplex recovers the pair via toReal on each component.
background
The module ComplexFromLogic constructs LogicComplex as pairs of recovered reals (via fromReal on each component) and supplies transport maps to and from Mathlib ℂ. The local setting is carrier-level equivalence only; analytic operations remain in Mathlib ℂ via the equivalence. Upstream results are the definitions fromComplex (pairs the real and imaginary parts after fromReal) and toComplex (applies toReal componentwise), together with the real-line theorem toReal_fromReal that toReal(fromReal x) = x.
proof idea
One-line wrapper that applies Complex.ext and then simp on the definitions toComplex, fromComplex together with toReal_fromReal.
why it matters
This supplies the right inverse for equivComplex (the carrier equivalence LogicComplex ≃ ℂ) and appears inside logicComplex_recovered_from_mathlib, which states that the recovered complex carrier is exactly Mathlib ℂ by transport. It closes the round-trip for the complex numbers recovered from the real line, consistent with the foundation pattern already established for reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.