mul_comm'
plain-language theorem explainer
Multiplication commutes on LogicReal, the wrapper around the Bourbaki completion of the recovered rationals. Foundation researchers cite this result when transporting ring identities from Mathlib reals back through the equivalence. The proof reduces the claim via the equality transport lemma and finishes with simp followed by ring on the underlying reals.
Claim. For all recovered reals $x, y$ in the Cauchy completion of the logic rationals, $x · y = y · x$.
background
The module recovers the reals from the Law-of-Logic layer by completing the recovered rationals LogicRat ≃ ℚ via Mathlib's Bourbakiℝ uniform-space completion. LogicReal is defined as a wrapper around CompareReals.Bourbakiℝ to avoid polluting global instances while still allowing reuse of completed-real theorems. The transport maps toReal and fromReal are the canonical equivalence, so algebraic statements on LogicReal reduce exactly to statements on the Mathlib reals.
proof idea
One-line wrapper that applies eq_iff_toReal_eq to convert the equality goal into an equality of underlying Bourbaki reals, then uses simp to expose the ring structure and ring to conclude commutativity.
why it matters
This theorem supplies the multiplicative commutativity needed for the real layer in the foundation chain, directly supporting the parallel mul_comm' statements in the integer and rational layers through the same transport pattern. It closes the algebraic recovery step from LogicRat to the completed reals, consistent with the module's transport-first design that lets every downstream theorem reduce to an existing Mathlib result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.