Documentation

Std.Data.Rat.Lemmas

Additional lemmas about the Rational Numbers #

source
theorem Rat.ext {p : Rat} {q : Rat} :
p.num = q.num → p.den = q.den → p = q
source
@[simp]
theorem Rat.mk_den_one {r : Int} :
{ num := r, den := 1, den_nz := Nat.one_ne_zero, reduced := ⋯ } = ↑r
source
@[simp]
theorem Rat.zero_num :
0.num = 0
source
@[simp]
theorem Rat.zero_den :
0.den = 1
source
@[simp]
theorem Rat.one_num :
1.num = 1
source
@[simp]
theorem Rat.one_den :
1.den = 1
source
@[simp]
theorem Rat.maybeNormalize_eq {num : Int} {den : Nat} {g : Nat} (den_nz : den / g ≠ 0) (reduced : Nat.Coprime (Int.natAbs (Int.div num ↑g)) (den / g)) :
Rat.maybeNormalize num den g den_nz reduced = { num := Int.div num ↑g, den := den / g, den_nz := den_nz, reduced := reduced }
source
theorem Rat.normalize.reduced' {num : Int} {den : Nat} {g : Nat} (den_nz : den ≠ 0) (e : g = Nat.gcd (Int.natAbs num) den) :
Nat.Coprime (Int.natAbs (num / ↑g)) (den / g)
source
theorem Rat.normalize_eq {num : Int} {den : Nat} (den_nz : den ≠ 0) :
Rat.normalize num den den_nz = { num := num / ↑(Nat.gcd (Int.natAbs num) den), den := den / Nat.gcd (Int.natAbs num) den, den_nz := ⋯, reduced := ⋯ }
source
@[simp]
theorem Rat.normalize_zero {d : Nat} (nz : d ≠ 0) :
Rat.normalize 0 d nz = 0
source
theorem Rat.mk_eq_normalize (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.Coprime (Int.natAbs num) den) :
{ num := num, den := den, den_nz := nz, reduced := c } = Rat.normalize num den nz
source
theorem Rat.normalize_self (r : Rat) :
Rat.normalize r.num r.den ⋯ = r
source
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
source
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
source
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₁
source
theorem Rat.maybeNormalize_eq_normalize {num : Int} {den : Nat} {g : Nat} (den_nz : den / g ≠ 0) (reduced : Nat.Coprime (Int.natAbs (Int.div num ↑g)) (den / g)) (hn : ↑g ∣ num) (hd : g ∣ den) :
Rat.maybeNormalize num den g den_nz reduced = Rat.normalize num den ⋯
source
@[simp]
theorem Rat.normalize_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) :
Rat.normalize n d d0 = 0 ↔ n = 0
source
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
source
theorem Rat.normalize_num_den {n : Int} {d : Nat} {z : d ≠ 0} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : Nat.Coprime (Int.natAbs n') 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
source
theorem Rat.normalize_eq_mkRat {num : Int} {den : Nat} (den_nz : den ≠ 0) :
Rat.normalize num den den_nz = mkRat num den
source
theorem Rat.mkRat_num_den {d : Nat} {n : Int} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : Nat.Coprime (Int.natAbs n') 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
source
theorem Rat.mkRat_def (n : Int) (d : Nat) :
mkRat n d = if d0 : d = 0 then 0 else Rat.normalize n d d0
source
theorem Rat.mkRat_self (a : Rat) :
mkRat a.num a.den = a
source
theorem Rat.mk_eq_mkRat (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.Coprime (Int.natAbs num) den) :
{ num := num, den := den, den_nz := nz, reduced := c } = mkRat num den
source
@[simp]
theorem Rat.zero_mkRat (n : Nat) :
mkRat 0 n = 0
source
@[simp]
theorem Rat.mkRat_zero (n : Int) :
mkRat n 0 = 0
source
theorem Rat.mkRat_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) :
mkRat n d = 0 ↔ n = 0
source
theorem Rat.mkRat_ne_zero {d : Nat} {n : Int} (d0 : d ≠ 0) :
mkRat n d ≠ 0 ↔ n ≠ 0
source
theorem Rat.mkRat_mul_left {n : Int} {d : Nat} {a : Nat} (a0 : a ≠ 0) :
mkRat (↑a * n) (a * d) = mkRat n d
source
theorem Rat.mkRat_mul_right {n : Int} {d : Nat} {a : Nat} (a0 : a ≠ 0) :
mkRat (n * ↑a) (d * a) = mkRat n d
source
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₁
source
@[simp]
theorem Rat.divInt_ofNat (num : Int) (den : Nat) :
Rat.divInt num ↑den = mkRat num den
source
theorem Rat.mk_eq_divInt (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.Coprime (Int.natAbs num) den) :
{ num := num, den := den, den_nz := nz, reduced := c } = Rat.divInt num ↑den
source
theorem Rat.divInt_self (a : Rat) :
Rat.divInt a.num ↑a.den = a
source
@[simp]
theorem Rat.zero_divInt (n : Int) :
Rat.divInt 0 n = 0
source
@[simp]
theorem Rat.divInt_zero (n : Int) :
Rat.divInt n 0 = 0
source
theorem Rat.neg_divInt_neg (num : Int) (den : Int) :
Rat.divInt (-num) (-den) = Rat.divInt num den
source
theorem Rat.divInt_neg' (num : Int) (den : Int) :
Rat.divInt num (-den) = Rat.divInt (-num) den
source
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₁
source
theorem Rat.divInt_mul_left {n : Int} {d : Int} {a : Int} (a0 : a ≠ 0) :
Rat.divInt (a * n) (a * d) = Rat.divInt n d
source
theorem Rat.divInt_mul_right {n : Int} {d : Int} {a : Int} (a0 : a ≠ 0) :
Rat.divInt (n * a) (d * a) = Rat.divInt n d
source
theorem Rat.divInt_num_den {d : Int} {n : Int} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : Nat.Coprime (Int.natAbs n') 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
source
@[simp]
theorem Rat.ofInt_ofNat {n : Nat} :
Rat.ofInt (OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem Rat.ofInt_num {n : Int} :
(Rat.ofInt n).num = n
source
@[simp]
theorem Rat.ofInt_den {n : Int} :
(Rat.ofInt n).den = 1
source
@[simp]
theorem Rat.ofNat_num {n : Nat} :
(OfNat.ofNat n).num = OfNat.ofNat n
source
@[simp]
theorem Rat.ofNat_den {n : Nat} :
(OfNat.ofNat n).den = 1
source
theorem Rat.add_def (a : Rat) (b : Rat) :
a + b = Rat.normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯
source
theorem Rat.add_def' (a : Rat) (b : Rat) :
a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)
source
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₂) ⋯
source
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₂)
source
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₂)
source
@[simp]
theorem Rat.neg_num (a : Rat) :
(-a).num = -a.num
source
@[simp]
theorem Rat.neg_den (a : Rat) :
(-a).den = a.den
source
theorem Rat.neg_normalize (n : Int) (d : Nat) (z : d ≠ 0) :
-Rat.normalize n d z = Rat.normalize (-n) d z
source
theorem Rat.neg_mkRat (n : Int) (d : Nat) :
-mkRat n d = mkRat (-n) d
source
theorem Rat.neg_divInt (n : Int) (d : Int) :
-Rat.divInt n d = Rat.divInt (-n) d
source
theorem Rat.sub_def (a : Rat) (b : Rat) :
a - b = Rat.normalize (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den) ⋯
source
theorem Rat.sub_def' (a : Rat) (b : Rat) :
a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)
source
theorem Rat.sub_eq_add_neg (a : Rat) (b : Rat) :
a - b = a + -b
source
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₂)
source
theorem Rat.mul_def (a : Rat) (b : Rat) :
a * b = Rat.normalize (a.num * b.num) (a.den * b.den) ⋯
source
theorem Rat.mul_comm (a : Rat) (b : Rat) :
a * b = b * a
source
@[simp]
theorem Rat.zero_mul (a : Rat) :
0 * a = 0
source
@[simp]
theorem Rat.mul_zero (a : Rat) :
a * 0 = 0
source
@[simp]
theorem Rat.one_mul (a : Rat) :
1 * a = a
source
@[simp]
theorem Rat.mul_one (a : Rat) :
a * 1 = a
source
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₂) ⋯
source
theorem Rat.mkRat_mul_mkRat (n₁ : Int) (n₂ : Int) (d₁ : Nat) (d₂ : Nat) :
mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
source
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₂)
source
theorem Rat.inv_def (a : Rat) :
Rat.inv a = Rat.divInt (↑a.den) a.num
source
@[simp]
theorem Rat.inv_zero :
Rat.inv 0 = 0
source
@[simp]
theorem Rat.inv_divInt (n : Int) (d : Int) :
Rat.inv (Rat.divInt n d) = Rat.divInt d n
source
theorem Rat.div_def (a : Rat) (b : Rat) :
a / b = a * Rat.inv b
source
theorem Rat.ofScientific_true_def {m : Nat} {e : Nat} :
Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)
source
theorem Rat.ofScientific_false_def {m : Nat} {e : Nat} :
Rat.ofScientific m false e = ↑(m * 10 ^ e)
source
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)
source
@[simp]
theorem Rat.intCast_den (a : Int) :
(↑a).den = 1
source
@[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.

source
@[simp]
theorem Rat.intCast_inj {a : Int} {b : Int} :
↑a = ↑b ↔ a = b
source
theorem Rat.intCast_zero :
↑0 = 0
source
theorem Rat.intCast_one :
↑1 = 1
source
@[simp]
theorem Rat.intCast_add (a : Int) (b : Int) :
↑(a + b) = ↑a + ↑b
source
@[simp]
theorem Rat.intCast_neg (a : Int) :
↑(-a) = -↑a
source
@[simp]
theorem Rat.intCast_sub (a : Int) (b : Int) :
↑(a - b) = ↑a - ↑b
source
@[simp]
theorem Rat.intCast_mul (a : Int) (b : Int) :
↑(a * b) = ↑a * ↑b