Documentation

Mathlib.Data.Rat.Lemmas

Further lemmas for the Rational Numbers #

theorem Rat.num_dvd (a : ℤ) {b : ℤ} (b0 : b ≠ 0) :

(divInt a b).num ∣ a

theorem Rat.den_dvd (a b : ℤ) :

↑(divInt a b).den ∣ b

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

@[deprecated Rat.num_divInt (since := "2025-12-27")]

theorem Rat.num_mk (n d : ℤ) :

(divInt n d).num = d.sign * n / ↑(n.gcd d)

@[deprecated Rat.den_divInt (since := "2025-12-27")]

theorem Rat.den_mk (n d : ℤ) :

(divInt n d).den = if d = 0 then 1 else d.natAbs / n.gcd d

theorem Rat.add_den_dvd_lcm (q₁ q₂ : ℚ) :

(q₁ + q₂).den ∣ q₁.den.lcm q₂.den

theorem Rat.sub_den_dvd_lcm (q₁ q₂ : ℚ) :

(q₁ - q₂).den ∣ q₁.den.lcm q₂.den

theorem Rat.add_den_dvd (q₁ q₂ : ℚ) :

(q₁ + q₂).den ∣ q₁.den * q₂.den

theorem Rat.sub_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)

@[simp]

theorem Rat.add_intCast_den (q : ℚ) (n : ℤ) :

(q + ↑n).den = q.den

@[simp]

theorem Rat.intCast_add_den (n : ℤ) (q : ℚ) :

(↑n + q).den = q.den

@[simp]

theorem Rat.sub_intCast_den (q : ℚ) (n : ℤ) :

(q - ↑n).den = q.den

@[simp]

theorem Rat.intCast_sub_den (n : ℤ) (q : ℚ) :

(↑n - q).den = q.den

@[simp]

theorem Rat.add_natCast_den (q : ℚ) (n : ℕ) :

(q + ↑n).den = q.den

@[simp]

theorem Rat.natCast_add_den (n : ℕ) (q : ℚ) :

(↑n + q).den = q.den

@[simp]

theorem Rat.sub_natCast_den (q : ℚ) (n : ℕ) :

(q - ↑n).den = q.den

@[simp]

theorem Rat.natCast_sub_den (n : ℕ) (q : ℚ) :

(↑n - q).den = q.den

@[simp]

theorem Rat.add_ofNat_den (q : ℚ) (n : ℕ) :

(q + OfNat.ofNat n).den = q.den

@[simp]

theorem Rat.ofNat_add_den (n : ℕ) (q : ℚ) :

(OfNat.ofNat n + q).den = q.den

@[simp]

theorem Rat.sub_ofNat_den (q : ℚ) (n : ℕ) :

(q - OfNat.ofNat n).den = q.den

@[simp]

theorem Rat.ofNat_sub_den (n : ℕ) (q : ℚ) :

(OfNat.ofNat n - q).den = q.den

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.

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.

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 = divInt (q.num * ↑r.den + ↑q.den * r.num) (↑q.den * ↑r.den)

theorem Rat.isSquare_iff {q : ℚ} :

IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

@[simp]

theorem Rat.isSquare_natCast_iff {n : ℕ} :

IsSquare ↑n ↔ IsSquare n

@[simp]

theorem Rat.isSquare_intCast_iff {z : ℤ} :

IsSquare ↑z ↔ IsSquare z

@[simp]

theorem Rat.isSquare_ofNat_iff {n : ℕ} :

IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)

theorem Rat.mkRat_add_mkRat_of_den (n₁ n₂ : ℤ) {d : ℕ} (h : d ≠ 0) :

mkRat n₁ d + mkRat n₂ d = mkRat (n₁ + n₂) d

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 : ℚ) :

(-q)⁻¹ = -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

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

theorem Rat.inv_intCast_num (a : ℤ) :

(↑a)⁻¹.num = a.sign

theorem Rat.inv_natCast_num (a : ℕ) :

(↑a)⁻¹.num = (↑a).sign

theorem Rat.inv_ofNat_num (a : ℕ) [a.AtLeastTwo] :

(OfNat.ofNat a)⁻¹.num = 1

theorem Rat.inv_intCast_den (a : ℤ) :

(↑a)⁻¹.den = if a = 0 then 1 else a.natAbs

theorem Rat.inv_natCast_den (a : ℕ) :

(↑a)⁻¹.den = if a = 0 then 1 else a

theorem Rat.inv_ofNat_den (a : ℕ) [a.AtLeastTwo] :

(OfNat.ofNat a)⁻¹.den = OfNat.ofNat a

theorem Rat.den_inv_of_ne_zero {q : ℚ} (hq : q ≠ 0) :

q⁻¹.den = q.num.natAbs

theorem Rat.forall {p : ℚ → Prop} :

(∀ (r : ℚ), p r) ↔ ∀ (a b : ℤ), b ≠ 0 → p (↑a / ↑b)

theorem Rat.exists {p : ℚ → Prop} :

(∃ (r : ℚ), p r) ↔ ∃ (a : ℤ) (b : ℤ), b ≠ 0 ∧ p (↑a / ↑b)

Denominator as `ℕ+` #

def Rat.pnatDen (x : ℚ) :

Denominator as ℕ+.

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 :

@[simp]

theorem Rat.pnatDen_zero :