Further lemmas for the Rational Numbers #

theorem Rat.num_dvd (a : ) {b : } (b0 : b 0) :
().num a
theorem Rat.den_dvd (a : ) (b : ) :
().den b
theorem Rat.num_den_mk {q : } {n : } {d : } (hd : d 0) (qdf : q = ) :
∃ (c : ), n = c * q.num d = c * q.den
theorem Rat.num_mk (n : ) (d : ) :
().num = d.sign * n / (n.gcd d)
theorem Rat.den_mk (n : ) (d : ) :
().den = if d = 0 then 1 else d.natAbs / n.gcd 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 / ((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
theorem Rat.mul_den (q₁ : ) (q₂ : ) :
(q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (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.isSquare_iff {q : } :
IsSquare q.num IsSquare q.den
@[simp]
@[simp]
@[simp]
theorem Rat.isSquare_ofNat_iff {n : } :
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_neg (q : ) :
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_self (n : ) :
(n / n) = n / n
theorem Rat.natCast_div_self (n : ) :
(n / n) = n / n
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
@[deprecated Rat.den_div_intCast_eq_one_iff]
theorem Rat.den_div_cast_eq_one_iff (m : ) (n : ) (hn : n 0) :
(m / n).den = 1 n m

Alias of Rat.den_div_intCast_eq_one_iff.

theorem Rat.inv_intCast_num_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.num = 1
theorem Rat.inv_natCast_num_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.num = 1
theorem Rat.inv_intCast_den_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.den = a
theorem Rat.inv_natCast_den_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.den = a
@[simp]
theorem Rat.inv_intCast_num (a : ) :
(a)⁻¹.num = a.sign
@[simp]
theorem Rat.inv_natCast_num (a : ) :
(a)⁻¹.num = (a).sign
@[simp]
theorem Rat.inv_ofNat_num (a : ) [a.AtLeastTwo] :
()⁻¹.num = 1
@[simp]
theorem Rat.inv_intCast_den (a : ) :
(a)⁻¹.den = if a = 0 then 1 else a.natAbs
@[simp]
theorem Rat.inv_natCast_den (a : ) :
(a)⁻¹.den = if a = 0 then 1 else a
@[deprecated Rat.intCast_div_self]
theorem Rat.coe_int_div_self (n : ) :
(n / n) = n / n

Alias of Rat.intCast_div_self.

@[deprecated Rat.natCast_div_self]
theorem Rat.coe_nat_div_self (n : ) :
(n / n) = n / n

Alias of Rat.natCast_div_self.

@[deprecated Rat.intCast_div]
theorem Rat.coe_int_div (a : ) (b : ) (h : b a) :
(a / b) = a / b

Alias of Rat.intCast_div.

@[deprecated Rat.natCast_div]
theorem Rat.coe_nat_div (a : ) (b : ) (h : b a) :
(a / b) = a / b

Alias of Rat.natCast_div.

@[deprecated Rat.inv_intCast_num_of_pos]
theorem Rat.inv_coe_int_num_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.num = 1

Alias of Rat.inv_intCast_num_of_pos.

@[deprecated Rat.inv_natCast_num_of_pos]
theorem Rat.inv_coe_nat_num_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.num = 1

Alias of Rat.inv_natCast_num_of_pos.

@[deprecated Rat.inv_intCast_den_of_pos]
theorem Rat.inv_coe_int_den_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.den = a

Alias of Rat.inv_intCast_den_of_pos.

@[deprecated Rat.inv_natCast_den_of_pos]
theorem Rat.inv_coe_nat_den_of_pos {a : } (ha0 : 0 < a) :
(a)⁻¹.den = a

Alias of Rat.inv_natCast_den_of_pos.

@[deprecated Rat.inv_intCast_num]
theorem Rat.inv_coe_int_num (a : ) :
(a)⁻¹.num = a.sign

Alias of Rat.inv_intCast_num.

@[deprecated Rat.inv_natCast_num]
theorem Rat.inv_coe_nat_num (a : ) :
(a)⁻¹.num = (a).sign

Alias of Rat.inv_natCast_num.

@[deprecated Rat.inv_intCast_den]
theorem Rat.inv_coe_int_den (a : ) :
(a)⁻¹.den = if a = 0 then 1 else a.natAbs

Alias of Rat.inv_intCast_den.

@[deprecated Rat.inv_natCast_den]
theorem Rat.inv_coe_nat_den (a : ) :
(a)⁻¹.den = if a = 0 then 1 else a

Alias of Rat.inv_natCast_den.

@[simp]
theorem Rat.inv_ofNat_den (a : ) [a.AtLeastTwo] :
()⁻¹.den =
theorem Rat.forall {p : } :
(∀ (r : ), p r) ∀ (a b : ), p (a / b)
theorem Rat.exists {p : } :
(∃ (r : ), p r) ∃ (a : ), ∃ (b : ), p (a / b)

Denominator as ℕ+#

def Rat.pnatDen (x : ) :

Denominator as ℕ+.

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