mul_comm'
plain-language theorem explainer
Commutativity of multiplication holds for all elements of LogicRat, the field of fractions of LogicInt. Researchers assembling the rational numbers from the logic primitives cite this lemma when verifying the commutative ring axioms before lifting to the reals. The proof reduces the statement to an equality in Mathlib's Rat via the transport map and the multiplication homomorphism, then closes with the ring tactic.
Claim. For all elements $a, b$ in the field of fractions of the integers constructed from logic, $a b = b a$.
background
LogicRat is the quotient of PreRat by the setoid ratRel, serving as the field of fractions of LogicInt. The module constructs these rationals after the integers are available from IntegersFromLogic. The upstream integers satisfy their own mul_comm' by the same reduction pattern using eq_iff_toInt_eq and toInt_mul. The transport lemma eq_iff_toRat_eq equates equality in LogicRat with equality of images under toRat, while toRat_mul records that this map is a ring homomorphism.
proof idea
The proof is a short tactic sequence. It rewrites the goal with eq_iff_toRat_eq to move to an equality in Rat. It then applies toRat_mul on both sides to obtain toRat a * toRat b = toRat b * toRat a. The ring tactic finishes the goal by commutativity in the target field.
why it matters
This lemma supplies the multiplicative commutativity axiom for LogicRat. It is invoked by ratRel_trans in the same module and by mul_comm' for LogicReal in RealsFromLogic. The result mirrors the earlier mul_comm' for LogicInt and completes the verification that LogicRat is a commutative ring. In the Recognition Science development this step ensures the rationals carry the algebraic structure required before the reals are formed and the forcing chain proceeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.