Documentation

Mathlib.Data.Rat.Lemmas

Further lemmas for the Rational Numbers #

theorem Rat.num_dvd (a : ) {b : } (b0 : b 0) :
(Rat.divInt a b).num a
theorem Rat.den_dvd (a : ) (b : ) :
(Rat.divInt a b).den b
theorem Rat.num_den_mk {q : } {n : } {d : } (hd : d 0) (qdf : q = Rat.divInt n d) :
∃ (c : ), n = c * q.num d = c * q.den
theorem Rat.num_mk (n : ) (d : ) :
(Rat.divInt n d).num = Int.sign d * n / (Int.gcd n d)
theorem Rat.den_mk (n : ) (d : ) :
(Rat.divInt n d).den = if d = 0 then 1 else Int.natAbs d / Int.gcd n d
theorem Rat.add_den_dvd (q₁ : ) (q₂ : ) :
(q₁ + q₂).den q₁.den * q₂.den
theorem Rat.mul_den_dvd (q₁ : ) (q₂ : ) :
(q₁ * q₂).den q₁.den * q₂.den
theorem Rat.mul_num (q₁ : ) (q₂ : ) :
(q₁ * q₂).num = q₁.num * q₂.num / (Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den))
theorem Rat.mul_den (q₁ : ) (q₂ : ) :
(q₁ * q₂).den = q₁.den * q₂.den / Nat.gcd (Int.natAbs (q₁.num * q₂.num)) (q₁.den * q₂.den)
theorem Rat.mul_self_num (q : ) :
(q * q).num = q.num * q.num
theorem Rat.mul_self_den (q : ) :
(q * q).den = q.den * q.den
theorem Rat.add_num_den (q : ) (r : ) :
q + r = Rat.divInt (q.num * r.den + q.den * r.num) (q.den * r.den)
theorem Rat.exists_eq_mul_div_num_and_eq_mul_div_den (n : ) {d : } (d_ne_zero : d 0) :
∃ (c : ), n = c * (n / d).num d = c * (n / d).den
theorem Rat.mul_num_den' (q : ) (r : ) :
(q * r).num * q.den * r.den = q.num * r.num * (q * r).den
theorem Rat.add_num_den' (q : ) (r : ) :
(q + r).num * q.den * r.den = (q.num * r.den + r.num * q.den) * (q + r).den
theorem Rat.substr_num_den' (q : ) (r : ) :
(q - r).num * q.den * r.den = (q.num * r.den - r.num * q.den) * (q - r).den
theorem Rat.inv_def'' {q : } :
q⁻¹ = q.den / q.num
theorem Rat.inv_neg (q : ) :
@[simp]
theorem Rat.mul_den_eq_num {q : } :
q * q.den = q.num
theorem Rat.den_div_cast_eq_one_iff (m : ) (n : ) (hn : n 0) :
(m / n).den = 1 n m
theorem Rat.num_div_eq_of_coprime {a : } {b : } (hb0 : 0 < b) (h : Nat.Coprime (Int.natAbs a) (Int.natAbs b)) :
(a / b).num = a
theorem Rat.den_div_eq_of_coprime {a : } {b : } (hb0 : 0 < b) (h : Nat.Coprime (Int.natAbs a) (Int.natAbs b)) :
(a / b).den = b
theorem Rat.div_int_inj {a : } {b : } {c : } {d : } (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprime (Int.natAbs a) (Int.natAbs b)) (h2 : Nat.Coprime (Int.natAbs c) (Int.natAbs d)) (h : a / b = c / d) :
a = c b = d
theorem Rat.coe_int_div_self (n : ) :
(n / n) = n / n
theorem Rat.coe_nat_div_self (n : ) :
(n / n) = n / n
theorem Rat.coe_int_div (a : ) (b : ) (h : b a) :
(a / b) = a / b
theorem Rat.coe_nat_div (a : ) (b : ) (h : b a) :
(a / b) = a / b
theorem Rat.inv_coe_int_num_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.num = 1
theorem Rat.inv_coe_nat_num_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.num = 1
theorem Rat.inv_coe_int_den_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.den = a
theorem Rat.inv_coe_nat_den_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.den = a
@[simp]
theorem Rat.inv_coe_int_num (a : ) :
(a)⁻¹.num = Int.sign a
@[simp]
theorem Rat.inv_coe_nat_num (a : ) :
(a)⁻¹.num = Int.sign a
@[simp]
@[simp]
theorem Rat.inv_coe_int_den (a : ) :
(a)⁻¹.den = if a = 0 then 1 else Int.natAbs a
@[simp]
theorem Rat.inv_coe_nat_den (a : ) :
(a)⁻¹.den = if a = 0 then 1 else a
theorem Rat.forall {p : Prop} :
(∀ (r : ), p r) ∀ (a b : ), p (a / b)
theorem Rat.exists {p : Prop} :
(∃ (r : ), p r) ∃ (a : ) (b : ), p (a / b)

Denominator as ℕ+ #

def Rat.pnatDen (x : ) :

Denominator as ℕ+.

Equations
Instances For
    @[simp]
    theorem Rat.coe_pnatDen (x : ) :
    (Rat.pnatDen x) = x.den
    theorem Rat.pnatDen_eq_iff_den_eq {x : } {n : ℕ+} :
    Rat.pnatDen x = n x.den = n
    @[simp]
    @[simp]