Documentation

Mathlib.Data.Rat.Lemmas

Further lemmas for the Rational Numbers #

source
theorem Rat.num_dvd (a : ℤ) {b : ℤ} (b0 : b ≠ 0) :
(Rat.divInt a b).num ∣ a
source
theorem Rat.den_dvd (a : ℤ) (b : ℤ) :
↑(Rat.divInt a b).den ∣ b
source
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
source
theorem Rat.num_mk (n : ℤ) (d : ℤ) :
(Rat.divInt n d).num = Int.sign d * n / ↑(Int.gcd n d)
source
theorem Rat.den_mk (n : ℤ) (d : ℤ) :
(Rat.divInt n d).den = if d = 0 then 1 else Int.natAbs d / Int.gcd n d
source
theorem Rat.add_den_dvd (q₁ : ℚ) (q₂ : ℚ) :
(q₁ + q₂).den ∣ q₁.den * q₂.den
source
theorem Rat.mul_den_dvd (q₁ : ℚ) (q₂ : ℚ) :
(q₁ * q₂).den ∣ q₁.den * q₂.den
source
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))
source
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)
source
theorem Rat.mul_self_num (q : ℚ) :
(q * q).num = q.num * q.num
source
theorem Rat.mul_self_den (q : ℚ) :
(q * q).den = q.den * q.den
source
theorem Rat.add_num_den (q : ℚ) (r : ℚ) :
q + r = Rat.divInt (q.num * ↑r.den + ↑q.den * r.num) (↑q.den * ↑r.den)
source
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
source
theorem Rat.mul_num_den' (q : ℚ) (r : ℚ) :
(q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
source
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
source
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
source
theorem Rat.inv_neg (q : ℚ) :
(-q)⁻¹ = -q⁻¹
source
@[simp]
theorem Rat.mul_den_eq_num {q : ℚ} :
q * ↑q.den = ↑q.num
source
theorem Rat.den_div_cast_eq_one_iff (m : ℤ) (n : ℤ) (hn : n ≠ 0) :
(↑m / ↑n).den = 1 ↔ n ∣ m
source
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
source
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
source
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
source
theorem Rat.intCast_div_self (n : ℤ) :
↑(n / n) = ↑n / ↑n
source
theorem Rat.natCast_div_self (n : ℕ) :
↑(n / n) = ↑n / ↑n
source
theorem Rat.intCast_div (a : ℤ) (b : ℤ) (h : b ∣ a) :
↑(a / b) = ↑a / ↑b
source
theorem Rat.natCast_div (a : ℕ) (b : ℕ) (h : b ∣ a) :
↑(a / b) = ↑a / ↑b
source
theorem Rat.inv_intCast_num_of_pos {a : ℤ} (ha0 : 0 < a) :
(↑a)⁻¹.num = 1
source
theorem Rat.inv_natCast_num_of_pos {a : ℕ} (ha0 : 0 < a) :
(↑a)⁻¹.num = 1
source
theorem Rat.inv_intCast_den_of_pos {a : ℤ} (ha0 : 0 < a) :
↑(↑a)⁻¹.den = a
source
theorem Rat.inv_natCast_den_of_pos {a : ℕ} (ha0 : 0 < a) :
(↑a)⁻¹.den = a
source
@[simp]
theorem Rat.inv_intCast_num (a : ℤ) :
(↑a)⁻¹.num = Int.sign a
source
@[simp]
theorem Rat.inv_natCast_num (a : ℕ) :
(↑a)⁻¹.num = Int.sign ↑a
source
@[simp]
theorem Rat.inv_ofNat_num (a : ℕ) [Nat.AtLeastTwo a] :
(OfNat.ofNat a)⁻¹.num = 1
source
@[simp]
theorem Rat.inv_intCast_den (a : ℤ) :
(↑a)⁻¹.den = if a = 0 then 1 else Int.natAbs a
source
@[simp]
theorem Rat.inv_natCast_den (a : ℕ) :
(↑a)⁻¹.den = if a = 0 then 1 else a
source
@[deprecated Rat.intCast_div_self]
theorem Rat.coe_int_div_self (n : ℤ) :
↑(n / n) = ↑n / ↑n

Alias of Rat.intCast_div_self.

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

Alias of Rat.natCast_div_self.

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

Alias of Rat.intCast_div.

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

Alias of Rat.natCast_div.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

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

Alias of Rat.inv_intCast_num.

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

Alias of Rat.inv_natCast_num.

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

Alias of Rat.inv_intCast_den.

source
@[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.

source
@[simp]
theorem Rat.inv_ofNat_den (a : ℕ) [Nat.AtLeastTwo a] :
(OfNat.ofNat a)⁻¹.den = OfNat.ofNat a
source
theorem Rat.forall {p : ℚ → Prop} :
(∀ (r : ℚ), p r) ↔ ∀ (a b : ℤ), p (↑a / ↑b)
source
theorem Rat.exists {p : ℚ → Prop} :
(∃ (r : ℚ), p r) ↔ ∃ (a : ℤ) (b : ℤ), p (↑a / ↑b)

Denominator as ℕ+ #

source
def Rat.pnatDen (x : ℚ) :
ℕ+

Denominator as ℕ+.

Equations
Instances For
    source
    @[simp]
    theorem Rat.coe_pnatDen (x : ℚ) :
    ↑(Rat.pnatDen x) = x.den
    source
    theorem Rat.pnatDen_eq_iff_den_eq {x : ℚ} {n : ℕ+} :
    Rat.pnatDen x = n ↔ x.den = ↑n
    source
    @[simp]
    theorem Rat.pnatDen_one :
    Rat.pnatDen 1 = 1
    source
    @[simp]
    theorem Rat.pnatDen_zero :
    Rat.pnatDen 0 = 1