CoqEAL rational/binrat, ported to Lean — num/den pairs refine ℚ

CoqEAL's rational refines MathComp rationals to numerator/denominator pairs. Here a pair ℤ × ℤ refines ℚ via toRat (division by zero folds to 0, so the relation is a total map, non-injective). The concrete componentwise product binMul refines ℚ multiplication — the CoqEAL Rmul square — and it holds unconditionally, without a den ≠ 0 side condition, because div_mul_div_comm is an identity in a division ring.

@[reducible, inline]

abbrev Transfer.Examples.CoqEAL.BinRat.BinRat : Type

A numerator/denominator pair, refining ℚ.

Equations

• Transfer.Examples.CoqEAL.BinRat.BinRat = (ℤ × ℤ)

def Transfer.Examples.CoqEAL.BinRat.toRat : BinRat → ℚ

Decode a pair to the rational it denotes (/ folds a zero denominator to 0).

Equations

• Transfer.Examples.CoqEAL.BinRat.toRat (n, d) = ↑n / ↑d

def Transfer.Examples.CoqEAL.BinRat.binMul : BinRat → BinRat → BinRat

Concrete multiplication: multiply numerators and denominators.

Equations

• Transfer.Examples.CoqEAL.BinRat.binMul (n₁, d₁) (n₂, d₂) = (n₁ * n₂, d₁ * d₂)

theorem Transfer.Examples.CoqEAL.BinRat.toRat_binMul (x y : BinRat) : toRat (binMul x y) = toRat x * toRat y

The CoqEAL Rmul refinement square. Componentwise multiplication of pairs refines ℚ multiplication: toRat (binMul x y) = toRat x * toRat y, unconditionally (via div_mul_div_comm).