mathlib3 documentation

data.rat.lemmas

Further lemmas for the Rational Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem rat.num_dvd (a : ) {b : } (b0 : b 0) :
(rat.mk a b).num a
theorem rat.denom_dvd (a b : ) :
((rat.mk a b).denom) b
theorem rat.num_denom_mk {q : } {n d : } (hd : d 0) (qdf : q = rat.mk n d) :
(c : ), n = c * q.num d = c * (q.denom)
theorem rat.mk_pnat_num (n : ) (d : ℕ+) :
theorem rat.mk_pnat_denom (n : ) (d : ℕ+) :
theorem rat.num_mk (n d : ) :
(rat.mk n d).num = d.sign * n / (n.gcd d)
theorem rat.denom_mk (n d : ) :
(rat.mk n d).denom = ite (d = 0) 1 (d.nat_abs / n.gcd d)
theorem rat.mk_pnat_denom_dvd (n : ) (d : ℕ+) :
theorem rat.add_denom_dvd (q₁ q₂ : ) :
(q₁ + q₂).denom q₁.denom * q₂.denom
theorem rat.mul_denom_dvd (q₁ q₂ : ) :
(q₁ * q₂).denom q₁.denom * q₂.denom
theorem rat.mul_num (q₁ q₂ : ) :
(q₁ * q₂).num = q₁.num * q₂.num / ((q₁.num * q₂.num).nat_abs.gcd (q₁.denom * q₂.denom))
theorem rat.mul_denom (q₁ q₂ : ) :
(q₁ * q₂).denom = q₁.denom * q₂.denom / (q₁.num * q₂.num).nat_abs.gcd (q₁.denom * q₂.denom)
theorem rat.mul_self_num (q : ) :
(q * q).num = q.num * q.num
theorem rat.mul_self_denom (q : ) :
(q * q).denom = q.denom * q.denom
theorem rat.add_num_denom (q r : ) :
q + r = rat.mk (q.num * (r.denom) + (q.denom) * r.num) ((q.denom) * (r.denom))
theorem rat.exists_eq_mul_div_num_and_eq_mul_div_denom (n : ) {d : } (d_ne_zero : d 0) :
(c : ), n = c * (n / d).num d = c * ((n / d).denom)
theorem rat.mul_num_denom' (q r : ) :
(q * r).num * (q.denom) * (r.denom) = q.num * r.num * ((q * r).denom)
theorem rat.add_num_denom' (q r : ) :
(q + r).num * (q.denom) * (r.denom) = (q.num * (r.denom) + r.num * (q.denom)) * ((q + r).denom)
theorem rat.substr_num_denom' (q r : ) :
(q - r).num * (q.denom) * (r.denom) = (q.num * (r.denom) - r.num * (q.denom)) * ((q - r).denom)
theorem rat.inv_def' {q : } :
@[protected]
theorem rat.inv_neg (q : ) :
@[simp]
theorem rat.mul_denom_eq_num {q : } :
q * (q.denom) = (q.num)
theorem rat.denom_div_cast_eq_one_iff (m n : ) (hn : n 0) :
(m / n).denom = 1 n m
theorem rat.num_div_eq_of_coprime {a b : } (hb0 : 0 < b) (h : a.nat_abs.coprime b.nat_abs) :
(a / b).num = a
theorem rat.denom_div_eq_of_coprime {a b : } (hb0 : 0 < b) (h : a.nat_abs.coprime b.nat_abs) :
((a / b).denom) = b
theorem rat.div_int_inj {a b c d : } (hb0 : 0 < b) (hd0 : 0 < d) (h1 : a.nat_abs.coprime b.nat_abs) (h2 : c.nat_abs.coprime d.nat_abs) (h : a / b = c / d) :
a = c b = d
@[norm_cast]
theorem rat.coe_int_div_self (n : ) :
(n / n) = n / n
@[norm_cast]
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) :
theorem rat.inv_coe_nat_num_of_pos {a : } (ha0 : 0 < a) :
theorem rat.inv_coe_int_denom_of_pos {a : } (ha0 : 0 < a) :
theorem rat.inv_coe_nat_denom_of_pos {a : } (ha0 : 0 < a) :
@[simp]
theorem rat.inv_coe_int_num (a : ) :
@[simp]
theorem rat.inv_coe_nat_num (a : ) :
@[simp]
theorem rat.inv_coe_int_denom (a : ) :
(a)⁻¹.denom = ite (a = 0) 1 a.nat_abs
@[simp]
theorem rat.inv_coe_nat_denom (a : ) :
(a)⁻¹.denom = ite (a = 0) 1 a
@[protected]
theorem rat.forall {p : Prop} :
( (r : ), p r) (a b : ), p (a / b)
@[protected]
theorem rat.exists {p : Prop} :
( (r : ), p r) (a b : ), p (a / b)

Denominator as ℕ+ #

def rat.pnat_denom (x : ) :

Denominator as ℕ+.

Equations
@[simp]
theorem rat.coe_pnat_denom (x : ) :
@[simp]
theorem rat.pnat_denom_one  :
@[simp]
theorem rat.pnat_denom_zero  :