PreRat

formal source

  37/-! ## 1. Pre-rational structure: pairs with non-zero denominator -/
  38
  39/-- A pre-rational is a pair `(num, den)` with `den ≠ 0`. -/
  40structure PreRat where
  41  num         : LogicInt
  42  den         : LogicInt
  43  den_nonzero : den ≠ 0
  44
  45/-- The field-of-fractions equivalence: `(a, b) ~ (c, d)` iff
  46`a * d = c * b`. -/
  47def ratRel : PreRat → PreRat → Prop :=
  48  fun p q => p.num * q.den = q.num * p.den
  49
  50theorem ratRel_refl : ∀ p : PreRat, ratRel p p := by
  51  intro p
  52  show p.num * p.den = p.num * p.den
  53  rfl
  54
  55theorem ratRel_symm : ∀ {p q : PreRat}, ratRel p q → ratRel q p := by
  56  intro p q h
  57  show q.num * p.den = p.num * q.den
  58  exact h.symm
  59
  60theorem ratRel_trans : ∀ {p q r : PreRat}, ratRel p q → ratRel q r → ratRel p r := by
  61  rintro ⟨a, b, hb⟩ ⟨c, d, hd⟩ ⟨e, f, hf⟩ hpq hqr
  62  -- hpq : a * d = c * b
  63  -- hqr : c * f = e * d
  64  -- goal: a * f = e * b
  65  -- Method: (a * f) * d = a * f * d = a * d * f = c * b * f = c * f * b = e * d * b = (e * b) * d.
  66  -- Cancel d ≠ 0.
  67  show a * f = e * b
  68  have key : (a * f) * d = (e * b) * d := by
  69    calc (a * f) * d
  70        = (a * d) * f := by rw [mul_assoc', mul_comm' f d, ← mul_assoc']