mathlib3 documentation

data.rat.lemmas

Further lemmas for the Rational Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

(rat.mk a b).num ∣ a

theorem rat.denom_dvd (a b : ℤ) :

↑((rat.mk a b).denom) ∣ b

theorem rat.num_denom_mk {q : ℚ} {n d : ℤ} (hd : d ≠ 0) (qdf : q = rat.mk n d) :

∃ (c : ℤ), n = c * q.num ∧ d = c * ↑(q.denom)

theorem rat.mk_pnat_num (n : ℤ) (d : ℕ+) :

(rat.mk_pnat n d).num = n / ↑(n.nat_abs.gcd ↑d)

theorem rat.mk_pnat_denom (n : ℤ) (d : ℕ+) :

(rat.mk_pnat n d).denom = ↑d / n.nat_abs.gcd ↑d

theorem rat.num_mk (n d : ℤ) :

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

theorem rat.denom_mk (n d : ℤ) :

(rat.mk n d).denom = ite (d = 0) 1 (d.nat_abs / n.gcd d)

theorem rat.mk_pnat_denom_dvd (n : ℤ) (d : ℕ+) :

(rat.mk_pnat n d).denom ∣ d.val

theorem rat.add_denom_dvd (q₁ q₂ : ℚ) :

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

theorem rat.mul_denom_dvd (q₁ q₂ : ℚ) :

(q₁ * q₂).denom ∣ q₁.denom * q₂.denom

theorem rat.mul_num (q₁ q₂ : ℚ) :

(q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).nat_abs.gcd (q₁.denom * q₂.denom))

theorem rat.mul_denom (q₁ q₂ : ℚ) :

(q₁ * q₂).denom = q₁.denom * q₂.denom / (q₁.num * q₂.num).nat_abs.gcd (q₁.denom * q₂.denom)

theorem rat.mul_self_num (q : ℚ) :

(q * q).num = q.num * q.num

theorem rat.mul_self_denom (q : ℚ) :

(q * q).denom = q.denom * q.denom

theorem rat.add_num_denom (q r : ℚ) :

q + r = rat.mk (q.num * ↑(r.denom) + ↑(q.denom) * r.num) (↑(q.denom) * ↑(r.denom))

theorem rat.exists_eq_mul_div_num_and_eq_mul_div_denom (n : ℤ) {d : ℤ} (d_ne_zero : d ≠ 0) :

∃ (c : ℤ), n = c * (↑n / ↑d).num ∧ d = c * ↑((↑n / ↑d).denom)

theorem rat.mul_num_denom' (q r : ℚ) :

(q * r).num * ↑(q.denom) * ↑(r.denom) = q.num * r.num * ↑((q * r).denom)

theorem rat.add_num_denom' (q r : ℚ) :

(q + r).num * ↑(q.denom) * ↑(r.denom) = (q.num * ↑(r.denom) + r.num * ↑(q.denom)) * ↑((q + r).denom)

theorem rat.substr_num_denom' (q r : ℚ) :

(q - r).num * ↑(q.denom) * ↑(r.denom) = (q.num * ↑(r.denom) - r.num * ↑(q.denom)) * ↑((q - r).denom)

theorem rat.inv_def' {q : ℚ} :

q⁻¹ = ↑(q.denom) / ↑(q.num)

@[protected]

theorem rat.inv_neg (q : ℚ) :

(-q)⁻¹ = -q⁻¹

@[simp]

theorem rat.mul_denom_eq_num {q : ℚ} :

q * ↑(q.denom) = ↑(q.num)

theorem rat.denom_div_cast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) :

(↑m / ↑n).denom = 1 ↔ n ∣ m

theorem rat.num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : a.nat_abs.coprime b.nat_abs) :

(↑a / ↑b).num = a

theorem rat.denom_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : a.nat_abs.coprime b.nat_abs) :

↑((↑a / ↑b).denom) = b

theorem rat.div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : a.nat_abs.coprime b.nat_abs) (h2 : c.nat_abs.coprime d.nat_abs) (h : ↑a / ↑b = ↑c / ↑d) :

a = c ∧ b = d

@[norm_cast]

theorem rat.coe_int_div_self (n : ℤ) :

↑(n / n) = ↑n / ↑n

@[norm_cast]

theorem rat.coe_nat_div_self (n : ℕ) :

↑(n / n) = ↑n / ↑n

theorem rat.coe_int_div (a b : ℤ) (h : b ∣ a) :

↑(a / b) = ↑a / ↑b

theorem rat.coe_nat_div (a b : ℕ) (h : b ∣ a) :

↑(a / b) = ↑a / ↑b

theorem rat.inv_coe_int_num_of_pos {a : ℤ} (ha0 : 0 < a) :

(↑a)⁻¹.num = 1

theorem rat.inv_coe_nat_num_of_pos {a : ℕ} (ha0 : 0 < a) :

(↑a)⁻¹.num = 1

theorem rat.inv_coe_int_denom_of_pos {a : ℤ} (ha0 : 0 < a) :

↑((↑a)⁻¹.denom) = a

theorem rat.inv_coe_nat_denom_of_pos {a : ℕ} (ha0 : 0 < a) :

(↑a)⁻¹.denom = a

@[simp]

theorem rat.inv_coe_int_num (a : ℤ) :

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

@[simp]

theorem rat.inv_coe_nat_num (a : ℕ) :

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

@[simp]

theorem rat.inv_coe_int_denom (a : ℤ) :

(↑a)⁻¹.denom = ite (a = 0) 1 a.nat_abs

@[simp]

theorem rat.inv_coe_nat_denom (a : ℕ) :

(↑a)⁻¹.denom = ite (a = 0) 1 a

@[protected]

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

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

@[protected]

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

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

Denominator as `ℕ+` #

def rat.pnat_denom (x : ℚ) :

Denominator as ℕ+.

Equations

x.pnat_denom = ⟨x.denom, _⟩

@[simp]

theorem rat.coe_pnat_denom (x : ℚ) :

↑(x.pnat_denom) = x.denom

@[simp]

theorem rat.mk_pnat_pnat_denom_eq (x : ℚ) :

rat.mk_pnat x.num x.pnat_denom = x

theorem rat.pnat_denom_eq_iff_denom_eq {x : ℚ} {n : ℕ+} :

x.pnat_denom = n ↔ x.denom = ↑n

@[simp]

theorem rat.pnat_denom_one :

1.pnat_denom = 1

@[simp]

theorem rat.pnat_denom_zero :

0.pnat_denom = 1