Fractions of nonnegative rationals

This file relates an arbitrary fraction a / b representing a nonnegative rational q to the reduced fraction q.num / q.den, and writes two nonnegative rationals over a common denominator. These let a statement phrased through q.num and q.den be checked on any fraction of q.

Main results

• TauCeti.NNRat.num_mul_eq_of_eq_div: q = a / b gives q.num * b = a * q.den.
• NNRat.eq_div_den_mul_den: q and q' as fractions over q.den * q'.den.

theorem TauCeti.NNRat.num_mul_eq_of_eq_div {q : ℚ≥0} {a b : ℕ} (hb : b ≠ 0) (hq : q = ↑a / ↑b) : q.num * b = a * q.den

Cross-multiplying with the reduced fraction: if q = a / b with b ≠ 0, then q.num * b = a * q.den.

theorem NNRat.eq_div_den_mul_den (q q' : ℚ≥0) : q = ↑(q.num * q'.den) / ↑(q.den * q'.den) ∧ q' = ↑(q'.num * q.den) / ↑(q.den * q'.den)

A common denominator: two nonnegative rationals q and q' are the fractions (q.num * q'.den) / (q.den * q'.den) and (q'.num * q.den) / (q.den * q'.den).