ratRel
plain-language theorem explainer
The field-of-fractions equivalence on pre-rationals identifies pairs with proportional numerators and denominators. Researchers building the rationals from integers would cite this predicate when forming the quotient. The implementation reduces directly to the cross-multiplication equality check on the pair components.
Claim. For pre-rationals $p = (a, b)$ and $q = (c, d)$ with $b, d$ nonzero, the relation holds precisely when $a d = c b$.
background
Pre-rational is the structure of a numerator-denominator pair drawn from LogicInt with the explicit nonzero-denominator hypothesis. The module constructs the rationals directly from the integers obtained via logic, using this relation as the first step toward the quotient type. The upstream PreRat structure supplies the pair components that enter the cross-multiplication test.
proof idea
The definition is a direct functional assignment returning the proposition that the cross products are equal. No lemmas or tactics are invoked; it is the primitive predicate for the equivalence.
why it matters
This equivalence supplies the relation that turns PreRat into a setoid, enabling the quotient that yields LogicRat as the field of fractions of LogicInt. It is invoked by the subsequent reflexivity, symmetry, and transitivity theorems and by the distributivity law add_mul'. In the Recognition framework it furnishes the rational arithmetic required for later constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.