add_mul'
plain-language theorem explainer
The theorem establishes distributivity of multiplication over addition on the recovered real numbers. Foundation proofs cite it when transporting ring identities from standard reals back through the logic layer. The proof reduces the claim via equality transport then dispatches it with simplification and the ring tactic.
Claim. For all recovered reals $x, y, z$, $(x + y) z = x z + y z$, where addition and multiplication are the operations induced on the Cauchy completion of the logic rationals.
background
The module recovers the real line from the law-of-logic rationals by completing the uniform space of LogicRat, which is equivalent to Q. LogicReal wraps Mathlib's Bourbaki completion of Q to isolate the recovered structure and reuse existing real theorems. The key transport lemma states that equality on LogicReal holds exactly when the images under the canonical map to the standard reals coincide.
proof idea
One-line wrapper that applies the equality transport lemma, simplifies the transported statement, and invokes the ring tactic on the standard reals.
why it matters
It supplies the distributive law required for the ring structure on the recovered reals, feeding the corresponding add_mul' results in the integers and rationals layers. The result closes the algebraic transport step in the reals-from-logic construction, consistent with the Bourbaki completion engine described in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.