Additional lemmas about the Rational Numbers

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

@[simp]

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

@[simp]

theorem Rat.zero_num : num 0 = 0

@[simp]

theorem Rat.zero_den : den 0 = 1

@[simp]

theorem Rat.one_num : num 1 = 1

@[simp]

theorem Rat.one_den : den 1 = 1

@[simp]

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

theorem Rat.normalize_eq {num : Int} {den : Nat} (den_nz : den ≠ 0) : 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) : 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 } = normalize num den nz

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

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

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

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

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

@[simp]

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

theorem Rat.normalize_num_den' (num : Int) (den : Nat) (nz : den ≠ 0) : ∃ (d : Nat), d ≠ 0 ∧ num = (normalize num den nz).num * ↑d ∧ den = (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 : 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) : normalize num den den_nz = mkRat num den

theorem Rat.mkRat_num_den {d : Nat} {n 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 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 a : Nat} (a0 : a ≠ 0) : mkRat (↑a * n) (a * d) = mkRat n d

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

theorem Rat.mkRat_eq_iff {d₁ d₂ : Nat} {n₁ 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) : 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 } = divInt num ↑den

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem Rat.divInt_num_den {d n n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (z : d ≠ 0) (h : 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} : ofInt (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem Rat.mkRat_add_mkRat (n₁ n₂ : Int) {d₁ 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₁ n₂ : Int) {d₁ d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : divInt n₁ d₁ + divInt n₂ d₂ = 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) : -normalize n d z = normalize (-n) d z

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

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

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

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

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

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

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

theorem Rat.mul_comm (a 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₁ n₂ : Int) {d₁ d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : normalize n₁ d₁ z₁ * normalize n₂ d₂ z₂ = normalize (n₁ * n₂) (d₁ * d₂) ⋯

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

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

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

@[simp]

theorem Rat.inv_zero : Rat.inv 0 = 0

@[simp]

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

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

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

theorem Rat.ofScientific_false_def {m 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 b : Int} : ↑a = ↑b ↔ a = b

theorem Rat.intCast_zero : ↑0 = 0

theorem Rat.intCast_one : ↑1 = 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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