div_eq
plain-language theorem explainer
The division notation on PRC rationals is definitionally the named division map built from multiplication and reciprocal. Anyone rewriting field expressions on ratio-orbit quotients will hit this simp rule. The proof is pure reflexivity: the Div instance is that map.
Claim. For PRC rationals $a,b$ (ratio-orbit quotient classes with nonzero denominator), the field notation $a/b$ equals the explicit division $a\cdot b^{-1}$.
background
PRC rationals are the K4.8 construction: nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator. They sit under the Primitive Recognition Calculus layer that builds arithmetic before the real completion.
Division on these classes is defined by multiplication against the reciprocal: $\mathrm{div}(a,b) := a\cdot b^{-1}$. The same pattern appears one level down on raw ratio orbits. A Div instance then installs the usual / notation for that map.
This module equips the quotient with field-like operations so later continuity and completeness results can treat PRC rationals as an ordered field seed.
proof idea
One-line reflexivity. The Div instance sets / to the named div, so a / b = div a b holds by definitional equality (rfl). No lemmas are applied.
why it matters
Simp infrastructure for the PRC rational field. Without the bridge from notation to the named map, downstream rewrites on products, reciprocals, and quotients would not fire uniformly. The module is assembling the arithmetic substrate that feeds the forcing chain's cost calculus (J-cost and the Recognition Composition Law live on positive reals built from this seed). No downstream theorems currently cite it directly; it is local notation hygiene inside RationalField.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.