Documentation

Mathlib.Data.Rat.Lemmas

Further lemmas for the Rational Numbers #

source
theorem Rat.num_dvd (a : ℤ) {b : ℤ} (b0 : b ≠ 0) :
(divInt a b).num ∣ a
source
theorem Rat.den_dvd (a b : ℤ) :
↑(divInt a b).den ∣ b
source
theorem Rat.num_den_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = divInt n d) :
∃ (c : ℤ), n = c * q.num ∧ d = c * ↑q.den
source
theorem Rat.num_mk (n d : ℤ) :
(divInt n d).num = d.sign * n / ↑(n.gcd d)
source
theorem Rat.den_mk (n d : ℤ) :
(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.den_mul_den_eq_den_mul_gcd (q₁ q₂ : ℚ) :
q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

A version of Rat.mul_den without division.

source
theorem Rat.num_mul_num_eq_num_mul_gcd (q₁ q₂ : ℚ) :
q₁.num * q₂.num = (q₁ * q₂).num * ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))

A version of Rat.mul_num without division.

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 = 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.mkRat_add_mkRat_of_den (n₁ n₂ : ℤ) {d : ℕ} (h : d ≠ 0) :
mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d
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
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
@[simp]
theorem Rat.inv_ofNat_den (a : ℕ) [a.AtLeastTwo] :
(OfNat.ofNat a)⁻¹.den = OfNat.ofNat a
source
theorem Rat.den_inv_of_ne_zero {q : ℚ} (hq : q ≠ 0) :
q⁻¹.den = q.num.natAbs
source
theorem Rat.num_inv (q : ℚ) :
q⁻¹.num = q.num.sign * ↑q.den
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 : ℚ) :
    ↑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 :
    pnatDen 1 = 1
    source
    @[simp]
    theorem Rat.pnatDen_zero :
    pnatDen 0 = 1