Additional lemmas about the Rational Numbers

theorem Rat.ext {p : Rat} {q : Rat} : p.num = q.num → p.den = q.den → p = q

@[simp]

theorem Rat.mk_den_one {r : Int} : { num := r, den := 1, den_nz := Nat.one_ne_zero, reduced := ⋯ } = ↑r

@[simp]

theorem Rat.zero_num : Rat.num 0 = 0

@[simp]

theorem Rat.zero_den : Rat.den 0 = 1

@[simp]

theorem Rat.one_num : Rat.num 1 = 1

@[simp]

theorem Rat.one_den : Rat.den 1 = 1

@[simp]

theorem Rat.maybeNormalize_eq {num : Int} {den : Nat} {g : Nat} (den_nz : den / g ≠ 0) (reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)) : Rat.maybeNormalize num den g den_nz reduced = { num := num.tdiv ↑g, den := den / g, den_nz := den_nz, reduced := reduced }

theorem Rat.normalize.reduced' {num : Int} {den : Nat} {g : Nat} (den_nz : den ≠ 0) (e : g = num.natAbs.gcd den) : (num / ↑g).natAbs.Coprime (den / g)

theorem Rat.normalize_eq {num : Int} {den : Nat} (den_nz : den ≠ 0) : Rat.normalize num den den_nz = { num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }

@[simp]

theorem Rat.normalize_zero {d : Nat} (nz : d ≠ 0) : Rat.normalize 0 d nz = 0

theorem Rat.mk_eq_normalize (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = Rat.normalize num den nz

theorem Rat.normalize_self (r : Rat) : Rat.normalize r.num r.den ⋯ = r

theorem Rat.normalize_mul_left {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) : Rat.normalize (↑a * n) (a * d) ⋯ = Rat.normalize n d d0

theorem Rat.normalize_mul_right {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) : Rat.normalize (n * ↑a) (d * a) ⋯ = Rat.normalize n d d0

theorem Rat.normalize_eq_iff {d₁ : Nat} {d₂ : Nat} {n₁ : Int} {n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : Rat.normalize n₁ d₁ z₁ = Rat.normalize n₂ d₂ z₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

theorem Rat.maybeNormalize_eq_normalize {num : Int} {den : Nat} {g : Nat} (den_nz : den / g ≠ 0) (reduced : (num.tdiv ↑g).natAbs.Coprime (den / g)) (hn : ↑g ∣ num) (hd : g ∣ den) : Rat.maybeNormalize num den g den_nz reduced = Rat.normalize num den ⋯

@[simp]

theorem Rat.normalize_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) : Rat.normalize n d d0 = 0 ↔ n = 0

theorem Rat.normalize_num_den' (num : Int) (den : Nat) (nz : den ≠ 0) : ∃ (d : Nat), d ≠ 0 ∧ num = (Rat.normalize num den nz).num * ↑d ∧ den = (Rat.normalize num den nz).den * d

theorem Rat.normalize_num_den {n : Int} {d : Nat} {z : d ≠ 0} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (h : Rat.normalize n d z = { num := n', den := d', den_nz := z', reduced := c }) : ∃ (m : Nat), m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

theorem Rat.normalize_eq_mkRat {num : Int} {den : Nat} (den_nz : den ≠ 0) : Rat.normalize num den den_nz = mkRat num den

theorem Rat.mkRat_num_den {d : Nat} {n : Int} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (z : d ≠ 0) (h : mkRat n d = { num := n', den := d', den_nz := z', reduced := c }) : ∃ (m : Nat), m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

theorem Rat.mkRat_def (n : Int) (d : Nat) : mkRat n d = if d0 : d = 0 then 0 else Rat.normalize n d d0

theorem Rat.mkRat_self (a : Rat) : mkRat a.num a.den = a

theorem Rat.mk_eq_mkRat (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = mkRat num den

@[simp]

theorem Rat.zero_mkRat (n : Nat) : mkRat 0 n = 0

@[simp]

theorem Rat.mkRat_zero (n : Int) : mkRat n 0 = 0

theorem Rat.mkRat_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) : mkRat n d = 0 ↔ n = 0

theorem Rat.mkRat_ne_zero {d : Nat} {n : Int} (d0 : d ≠ 0) : mkRat n d ≠ 0 ↔ n ≠ 0

theorem Rat.mkRat_mul_left {n : Int} {d : Nat} {a : Nat} (a0 : a ≠ 0) : mkRat (↑a * n) (a * d) = mkRat n d

theorem Rat.mkRat_mul_right {n : Int} {d : Nat} {a : Nat} (a0 : a ≠ 0) : mkRat (n * ↑a) (d * a) = mkRat n d

theorem Rat.mkRat_eq_iff {d₁ : Nat} {d₂ : Nat} {n₁ : Int} {n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

@[simp]

theorem Rat.divInt_ofNat (num : Int) (den : Nat) : Rat.divInt num ↑den = mkRat num den

theorem Rat.mk_eq_divInt (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = Rat.divInt num ↑den

theorem Rat.divInt_self (a : Rat) : Rat.divInt a.num ↑a.den = a

@[simp]

theorem Rat.zero_divInt (n : Int) : Rat.divInt 0 n = 0

@[simp]

theorem Rat.divInt_zero (n : Int) : Rat.divInt n 0 = 0

theorem Rat.neg_divInt_neg (num : Int) (den : Int) : Rat.divInt (-num) (-den) = Rat.divInt num den

theorem Rat.divInt_neg' (num : Int) (den : Int) : Rat.divInt num (-den) = Rat.divInt (-num) den

theorem Rat.divInt_eq_iff {d₁ : Int} {d₂ : Int} {n₁ : Int} {n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : Rat.divInt n₁ d₁ = Rat.divInt n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

theorem Rat.divInt_mul_left {n : Int} {d : Int} {a : Int} (a0 : a ≠ 0) : Rat.divInt (a * n) (a * d) = Rat.divInt n d

theorem Rat.divInt_mul_right {n : Int} {d : Int} {a : Int} (a0 : a ≠ 0) : Rat.divInt (n * a) (d * a) = Rat.divInt n d

theorem Rat.divInt_num_den {d : Int} {n : Int} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (z : d ≠ 0) (h : Rat.divInt n d = { num := n', den := d', den_nz := z', reduced := c }) : ∃ (m : Int), m ≠ 0 ∧ n = n' * m ∧ d = ↑d' * m

@[simp]

theorem Rat.ofInt_ofNat {n : Nat} : Rat.ofInt (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Rat.ofInt_num {n : Int} : (Rat.ofInt n).num = n

@[simp]

theorem Rat.ofInt_den {n : Int} : (Rat.ofInt n).den = 1

@[simp]

theorem Rat.ofNat_num {n : Nat} : Rat.num (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Rat.ofNat_den {n : Nat} : Rat.den (OfNat.ofNat n) = 1

theorem Rat.add_def (a : Rat) (b : Rat) : a + b = Rat.normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

theorem Rat.add_def' (a : Rat) (b : Rat) : a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)

theorem Rat.normalize_add_normalize (n₁ : Int) (n₂ : Int) {d₁ : Nat} {d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : Rat.normalize n₁ d₁ z₁ + Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯

theorem Rat.mkRat_add_mkRat (n₁ : Int) (n₂ : Int) {d₁ : Nat} {d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂)

theorem Rat.divInt_add_divInt (n₁ : Int) (n₂ : Int) {d₁ : Int} {d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : Rat.divInt n₁ d₁ + Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂ + n₂ * d₁) (d₁ * d₂)

@[simp]

theorem Rat.neg_num (a : Rat) : (-a).num = -a.num

@[simp]

theorem Rat.neg_den (a : Rat) : (-a).den = a.den

theorem Rat.neg_normalize (n : Int) (d : Nat) (z : d ≠ 0) : -Rat.normalize n d z = Rat.normalize (-n) d z

theorem Rat.neg_mkRat (n : Int) (d : Nat) : -mkRat n d = mkRat (-n) d

theorem Rat.neg_divInt (n : Int) (d : Int) : -Rat.divInt n d = Rat.divInt (-n) d

theorem Rat.sub_def (a : Rat) (b : Rat) : a - b = Rat.normalize (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den) ⋯

theorem Rat.sub_def' (a : Rat) (b : Rat) : a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)

theorem Rat.sub_eq_add_neg (a : Rat) (b : Rat) : a - b = a + -b

theorem Rat.divInt_sub_divInt (n₁ : Int) (n₂ : Int) {d₁ : Int} {d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : Rat.divInt n₁ d₁ - Rat.divInt n₂ d₂ = Rat.divInt (n₁ * d₂ - n₂ * d₁) (d₁ * d₂)

theorem Rat.mul_def (a : Rat) (b : Rat) : a * b = Rat.normalize (a.num * b.num) (a.den * b.den) ⋯

theorem Rat.mul_comm (a : Rat) (b : Rat) : a * b = b * a

@[simp]

theorem Rat.zero_mul (a : Rat) : 0 * a = 0

@[simp]

theorem Rat.mul_zero (a : Rat) : a * 0 = 0

@[simp]

theorem Rat.one_mul (a : Rat) : 1 * a = a

@[simp]

theorem Rat.mul_one (a : Rat) : a * 1 = a

theorem Rat.normalize_mul_normalize (n₁ : Int) (n₂ : Int) {d₁ : Nat} {d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : Rat.normalize n₁ d₁ z₁ * Rat.normalize n₂ d₂ z₂ = Rat.normalize (n₁ * n₂) (d₁ * d₂) ⋯

theorem Rat.mkRat_mul_mkRat (n₁ : Int) (n₂ : Int) (d₁ : Nat) (d₂ : Nat) : mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

theorem Rat.divInt_mul_divInt (n₁ : Int) (n₂ : Int) {d₁ : Int} {d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : Rat.divInt n₁ d₁ * Rat.divInt n₂ d₂ = Rat.divInt (n₁ * n₂) (d₁ * d₂)

theorem Rat.inv_def (a : Rat) : a.inv = Rat.divInt (↑a.den) a.num

@[simp]

theorem Rat.inv_zero : Rat.inv 0 = 0

@[simp]

theorem Rat.inv_divInt (n : Int) (d : Int) : (Rat.divInt n d).inv = Rat.divInt d n

theorem Rat.div_def (a : Rat) (b : Rat) : a / b = a * b.inv

theorem Rat.ofScientific_true_def {m : Nat} {e : Nat} : Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)

theorem Rat.ofScientific_false_def {m : Nat} {e : Nat} : Rat.ofScientific m false e = ↑(m * 10 ^ e)

theorem Rat.ofScientific_def {m : Nat} {s : Bool} {e : Nat} : Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

@[simp]

theorem Rat.ofScientific_ofNat_ofNat {m : Nat} {s : Bool} {e : Nat} : Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e

Rat.ofScientific applied to numeric literals is the same as a scientific literal.

@[simp]

theorem Rat.intCast_den (a : Int) : (↑a).den = 1

@[simp]

theorem Rat.intCast_num (a : Int) : (↑a).num = a

The following lemmas are later subsumed by e.g. Int.cast_add and Int.cast_mul in Mathlib but it is convenient to have these earlier, for users who only need Int and Rat.

@[simp]

theorem Rat.intCast_inj {a : Int} {b : Int} : ↑a = ↑b ↔ a = b

theorem Rat.intCast_zero : ↑0 = 0

theorem Rat.intCast_one : ↑1 = 1

@[simp]

theorem Rat.intCast_add (a : Int) (b : Int) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem Rat.intCast_neg (a : Int) : ↑(-a) = -↑a

@[simp]

theorem Rat.intCast_sub (a : Int) (b : Int) : ↑(a - b) = ↑a - ↑b

@[simp]

theorem Rat.intCast_mul (a : Int) (b : Int) : ↑(a * b) = ↑a * ↑b