toReal_inv
plain-language theorem explainer
The transport map from LogicReal to standard reals preserves multiplicative inverses. Researchers recovering field structure from the logic layer cite this when moving algebraic identities across the equivalence. The proof is a one-line wrapper that applies the round-trip lemma toReal_fromReal after expressing the inverse via fromReal.
Claim. For every $x$ in the recovered reals, the transport satisfies $toReal(x^{-1}) = (toReal x)^{-1}$.
background
The module recovers the reals from the Law-of-Logic rationals by completing LogicRat to LogicReal via Mathlib's Bourbaki completion of ℚ. LogicReal wraps CompareReals.Bourbakiℝ to avoid global instance pollution while reusing the completed real line. The map toReal is the canonical comparison equivalence sending a LogicReal to its image in ℝ.
proof idea
The proof is a one-line wrapper that applies toReal_fromReal after rewriting the inverse on LogicReal in terms of fromReal.
why it matters
This lemma ensures field operations on LogicReal transport correctly to ℝ, supporting the transport-first API in the module. It closes part of the equivalence between recovered and standard reals, allowing downstream theorems to reduce to existing real-number results and read back as recovered theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.