Documentation

Batteries.Data.Rat.Lemmas

Additional lemmas about the Rational Numbers #

theorem Rat.ext {p : Rat} {q : Rat} :
p.num = q.nump.den = q.denp = 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 :
@[simp]
theorem Rat.zero_den :
@[simp]
theorem Rat.one_num :
@[simp]
theorem Rat.one_den :
@[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) :
@[simp]
theorem Rat.divInt_zero (n : Int) :
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_num {n : Int} :
(Rat.ofInt n).num = n
@[simp]
theorem Rat.ofInt_den {n : Int} :
(Rat.ofInt n).den = 1
@[simp]
theorem Rat.ofNat_den {n : Nat} :
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) :
theorem Rat.neg_mkRat (n : Int) (d : Nat) :
-mkRat n d = mkRat (-n) d
theorem Rat.neg_divInt (n : Int) (d : Int) :
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 :
@[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]

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