toComplex_mul
plain-language theorem explainer
The theorem states that the transport map from logic-built complex numbers to Mathlib's ℂ preserves multiplication. Researchers verifying the ring isomorphism between recovered arithmetic and standard complex numbers would cite it when checking multiplicative compatibility. The proof is a one-line simp wrapper that unfolds the multiplication instances on both sides.
Claim. For recovered complex numbers $z, w$ (pairs of recovered reals), the transport satisfies $toComplex(z · w) = toComplex(z) · toComplex(w)$ in Mathlib's ℂ.
background
LogicComplex is the structure whose fields are a recovered real part and imaginary part. The map toComplex sends such a pair to the corresponding element of ℂ by applying toReal to each component. Multiplication on LogicComplex is defined via the lifted operations from the integer and rational layers, which in turn rest on the recursive multiplication defined on LogicNat.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the hints HMul.hMul and Mul.mul. This reduces both sides to the underlying componentwise arithmetic, where the equality is immediate from the definitions of multiplication on the recovered reals.
why it matters
The result confirms that toComplex is a multiplicative homomorphism, completing one half of the carrier equivalence between the logic complex numbers and Mathlib's ℂ. It sits in the foundation layer that recovers standard arithmetic before any analytic work begins. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.