one_mul'
plain-language theorem explainer
The theorem establishes that multiplication by the unit leaves any element of the recovered real line unchanged. Researchers tracing the logic-to-reals recovery chain cite it to confirm the multiplicative identity survives completion. The proof reduces the claim to the corresponding identity on Mathlib's reals via the transport equivalence and discharges it by simplification.
Claim. For every element $x$ of the logic-real line, $1 · x = x$.
background
LogicReal is the Cauchy completion of the recovered rationals, realized as a wrapper around Mathlib's Bourbaki completion of ℚ after the equivalence LogicRat ≃ ℚ. The module recovers the reals by completing the logic rationals while defining algebra and order by pullback along the transport map toReal, so every identity reduces to its Mathlib counterpart and is read back. Upstream results include the one_mul' theorems for LogicInt and LogicRat, which establish the identity at the integer and rational layers, together with the equality transfer lemma that equates recovered equality with equality after transport.
proof idea
The proof is a one-line wrapper that rewrites the goal using the equality transfer lemma eq_iff_toReal_eq, converting the statement into an identity on the standard real line, then applies simp to close it.
why it matters
This declaration supplies the multiplicative unit property at the completed real level and is referenced by the one_mul' declarations in the integer and rational modules. It closes the algebraic recovery step from the Law of Logic through naturals, integers and rationals to the reals via Bourbaki completion, ensuring the structure is preserved under transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.