div_mul_cancel
plain-language theorem explainer
For primitive recognition rationals, multiplying a quotient on the right by its divisor recovers the original value whenever the divisor has nonzero rational display. Field-structure work on the PRC rationals cites this cancellation law. The proof pushes the identity through the injective display map into ordinary rationals and finishes by field simplification.
Claim. Let $a,b$ be primitive recognition rationals (ratio-orbit quotient classes). If the rational display of $b$ is nonzero, then $(a/b)\cdot b = a$.
background
Primitive recognition rationals are the K4.8 quotient of ratio orbits by the cross-multiplication setoid: two displays represent the same class when numerators and denominators cross-multiply equally, with nonzero denominators. The verifier map toRat sends a class to an ordinary rational $\mathbb{Q}$ by the integer numerator over the natural denominator; it is a pure transport wrapper whose internal equality is cross-multiplication.
That display is injective on the quotient, so equalities of PRC rationals may be proved by comparing images in $\mathbb{Q}$. Multiplication and division on the quotient are defined so that the display is a homomorphism: the image of a product is the product of images, and the image of a quotient is the quotient of images. The present lemma is the standard right-cancellation identity for that division, under the nonzero-display hypothesis.
proof idea
One short tactic proof. Apply injectivity of the rational display so it suffices to check equality after toRat. Rewrite the left-hand side with the multiplicative and divisive compatibility lemmas, obtaining the ordinary identity $(a^{\mathbb{Q}}/b^{\mathbb{Q}})\cdot b^{\mathbb{Q}}=a^{\mathbb{Q}}$. Discharge that with field_simp using the hypothesis that the display of $b$ is nonzero.
why it matters
This is a basic field axiom for the PRC rational layer in Foundation.PrimitiveRecognitionCalculus. Downstream, OrbitEuclidean uses the same cancellation pattern when recovering natural values of quotient-times-divisor under a divides hypothesis (quotient_mul_divisor_toNat_of_divides). Without right-cancellation of division, later real-completeness and continuity modules that treat PRCRat as a field substrate cannot transport ordinary rational identities back to the orbit quotient. It sits well below the forcing chain (T5–T8) but is part of the arithmetic scaffolding those landmarks presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.