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 = d.sign * n / ↑(n.gcd d)
source
theorem Rat.den_mk (n d : ℤ) :
(Rat.divInt n d).den = if d = 0 then 1 else d.natAbs / n.gcd d
source
theorem Rat.add_den_dvd_lcm (q₁ q₂ : ℚ) :
(q₁ + q₂).den ∣ q₁.den.lcm q₂.den
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 / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
source
theorem Rat.mul_den (q₁ q₂ : ℚ) :
(q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (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.isSquare_iff {q : ℚ} :
IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den
source
@[simp]
theorem Rat.isSquare_natCast_iff {n : ℕ} :
IsSquare ↑n ↔ IsSquare n
source
@[simp]
theorem Rat.isSquare_intCast_iff {z : ℤ} :
IsSquare ↑z ↔ IsSquare z
source
@[simp]
theorem Rat.isSquare_ofNat_iff {n : ℕ} :
IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)
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
theorem Rat.num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : a.natAbs.Coprime b.natAbs) :
(↑a / ↑b).num = a
source
theorem Rat.den_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : a.natAbs.Coprime b.natAbs) :
↑(↑a / ↑b).den = b
source
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
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.den_div_intCast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) :
(↑m / ↑n).den = 1 ↔ n ∣ m
source
theorem Rat.den_div_natCast_eq_one_iff (m n : ℕ) (hn : n ≠ 0) :
(↑m / ↑n).den = 1 ↔ n ∣ m
source
@[deprecated Rat.den_div_intCast_eq_one_iff (since := "2024-05-11")]
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.

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 = a.sign
source
@[simp]
theorem Rat.inv_natCast_num (a : ℕ) :
(↑a)⁻¹.num = (↑a).sign
source
@[simp]
theorem Rat.inv_ofNat_num (a : ℕ) [a.AtLeastTwo] :
(OfNat.ofNat a)⁻¹.num = 1
source
@[simp]
theorem Rat.inv_intCast_den (a : ℤ) :
(↑a)⁻¹.den = if a = 0 then 1 else a.natAbs
source
@[simp]
theorem Rat.inv_natCast_den (a : ℕ) :
(↑a)⁻¹.den = if a = 0 then 1 else a
source
@[deprecated Rat.intCast_div_self (since := "2024-04-05")]
theorem Rat.coe_int_div_self (n : ℤ) :
↑(n / n) = ↑n / ↑n

Alias of Rat.intCast_div_self.

source
@[deprecated Rat.natCast_div_self (since := "2024-04-05")]
theorem Rat.coe_nat_div_self (n : ℕ) :
↑(n / n) = ↑n / ↑n

Alias of Rat.natCast_div_self.

source
@[deprecated Rat.intCast_div (since := "2024-04-05")]
theorem Rat.coe_int_div (a b : ℤ) (h : b ∣ a) :
↑(a / b) = ↑a / ↑b

Alias of Rat.intCast_div.

source
@[deprecated Rat.natCast_div (since := "2024-04-05")]
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 (since := "2024-04-05")]
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 (since := "2024-04-05")]
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 (since := "2024-04-05")]
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 (since := "2024-04-05")]
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 (since := "2024-04-05")]
theorem Rat.inv_coe_int_num (a : ℤ) :
(↑a)⁻¹.num = a.sign

Alias of Rat.inv_intCast_num.

source
@[deprecated Rat.inv_natCast_num (since := "2024-04-05")]
theorem Rat.inv_coe_nat_num (a : ℕ) :
(↑a)⁻¹.num = (↑a).sign

Alias of Rat.inv_natCast_num.

source
@[deprecated Rat.inv_intCast_den (since := "2024-04-05")]
theorem Rat.inv_coe_int_den (a : ℤ) :
(↑a)⁻¹.den = if a = 0 then 1 else a.natAbs

Alias of Rat.inv_intCast_den.

source
@[deprecated Rat.inv_natCast_den (since := "2024-04-05")]
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 : ℕ) [a.AtLeastTwo] :
(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
  • x.pnatDen = ⟨x.den, ⋯⟩
Instances For
    source
    @[simp]
    theorem Rat.coe_pnatDen (x : ℚ) :
    ↑x.pnatDen = x.den
    source
    theorem Rat.pnatDen_eq_iff_den_eq {x : ℚ} {n : ℕ+} :
    x.pnatDen = n ↔ x.den = ↑n
    source
    @[simp]
    theorem Rat.pnatDen_one :
    Rat.pnatDen 1 = 1
    source
    @[simp]
    theorem Rat.pnatDen_zero :
    Rat.pnatDen 0 = 1