Documentation

Mathlib.Data.Rat.Lemmas

Further lemmas for the Rational Numbers #

theorem Rat.num_dvd (a : ) {b : } (b0 : b 0) :
(divInt a b).num a
theorem Rat.den_dvd (a b : ) :
theorem Rat.num_den_mk {q : } {n d : } (hd : d 0) (qdf : q = divInt n d) :
theorem Rat.num_mk (n d : ) :
(divInt n d).num = d.sign * n / (n.gcd d)
theorem Rat.den_mk (n d : ) :
theorem Rat.add_den_dvd_lcm (q₁ q₂ : ) :
(q₁ + q₂).den q₁.den.lcm q₂.den
theorem Rat.add_den_dvd (q₁ q₂ : ) :
theorem Rat.mul_den_dvd (q₁ q₂ : ) :
theorem Rat.mul_num (q₁ q₂ : ) :
(q₁ * q₂).num = q₁.num * q₂.num / ((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
theorem Rat.mul_den (q₁ q₂ : ) :
theorem Rat.add_num_den (q r : ) :
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.num_div_eq_of_coprime {a b : } (hb0 : 0 < b) (h : a.natAbs.Coprime b.natAbs) :
(a / b).num = a
theorem Rat.den_div_eq_of_coprime {a b : } (hb0 : 0 < b) (h : a.natAbs.Coprime b.natAbs) :
(a / b).den = b
theorem Rat.div_int_inj {a b c d : } (hb0 : 0 < b) (hd0 : 0 < d) (h1 : a.natAbs.Coprime b.natAbs) (h2 : c.natAbs.Coprime d.natAbs) (h : a / b = c / d) :
a = c b = d
theorem Rat.intCast_div (a b : ) (h : b a) :
(a / b) = a / b
theorem Rat.natCast_div (a b : ) (h : b a) :
(a / b) = a / b
theorem Rat.den_div_intCast_eq_one_iff (m n : ) (hn : n 0) :
(m / n).den = 1 n m
theorem Rat.den_div_natCast_eq_one_iff (m n : ) (hn : n 0) :
(m / n).den = 1 n m
@[simp]
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]
    @[simp]
    @[simp]