data.rat.basic

Basics for the Rational Numbers #

Summary #

We define a rational number q as a structure { num, denom, pos, cop }, where

• num is the numerator of q,
• denom is the denominator of q,
• pos is a proof that denom > 0, and
• cop is a proof num and denom are coprime.

We then define the expected (discrete) field structure on ℚ and prove basic lemmas about it. Moreoever, we provide the expected casts from ℕ and ℤ into ℚ, i.e. (↑n : ℚ) = n / 1.

Main Definitions #

• rat is the structure encoding ℚ.
• rat.mk n d constructs a rational number q = n / d from n d : ℤ.

Notations #

• /. is infix notation for rat.mk.

Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom

structure rat  :
Type

rat, or ℚ, is the type of rational numbers. It is defined as the set of pairs ⟨n, d⟩ of integers such that d is positive and n and d are coprime. This representation is preferred to the quotient because without periodic reduction, the numerator and denominator can grow exponentially (for example, adding 1/2 to itself repeatedly).

Instances for rat
@[protected]
def rat.repr  :

String representation of a rational numbers, used in has_repr, has_to_string, and has_to_format instances.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
meta def rat.has_to_format  :
@[protected, instance]
Equations
def rat.of_int (n : ) :

Embed an integer as a rational number

Equations
@[protected, instance]
Equations
@[protected, instance]
def rat.has_one  :
Equations
@[protected, instance]
Equations
theorem rat.ext_iff {p q : } :
p = q p.num = q.num p.denom = q.denom
@[ext]
theorem rat.ext {p q : } (hn : p.num = q.num) (hd : p.denom = q.denom) :
p = q
def rat.mk_pnat (n : ) :
ℕ+

Form the quotient n / d where n:ℤ and d:ℕ+ (not necessarily coprime)

Equations
def rat.mk_nat (n : ) (d : ) :

Form the quotient n / d where n:ℤ and d:ℕ. In the case d = 0, we define n / 0 = 0 by convention.

Equations
• d = dite (d = 0) (λ (d0 : d = 0), 0) (λ (d0 : ¬d = 0), d, _⟩)
def rat.mk  :

Form the quotient n / d where n d : ℤ.

Equations
theorem rat.mk_pnat_eq (n : ) (d : ) (h : 0 < d) :
d, h⟩ = d
theorem rat.mk_nat_eq (n : ) (d : ) :
d = d
@[simp]
theorem rat.mk_zero (n : ) :
0 = 0
@[simp]
theorem rat.zero_mk_pnat (n : ℕ+) :
n = 0
@[simp]
theorem rat.zero_mk_nat (n : ) :
n = 0
@[simp]
theorem rat.zero_mk (n : ) :
n = 0
@[simp]
theorem rat.mk_eq_zero {a b : } (b0 : b 0) :
b = 0 a = 0
theorem rat.mk_ne_zero {a b : } (b0 : b 0) :
b 0 a 0
theorem rat.mk_eq {a b c d : } (hb : b 0) (hd : d 0) :
b = d a * d = c * b
@[simp]
theorem rat.div_mk_div_cancel_left {a b c : } (c0 : c 0) :
rat.mk (a * c) (b * c) = b
@[simp]
theorem rat.num_denom {a : } :
(a.denom) = a
theorem rat.num_denom' {n : } {d : } {h : 0 < d} {c : n.nat_abs.coprime d} :
{num := n, denom := d, pos := h, cop := c} = d
theorem rat.of_int_eq_mk (z : ) :
= 1
def rat.num_denom_cases_on {C : Sort u} (a : ) (H : Π (n : ) (d : ), 0 < dn.nat_abs.coprime dC (rat.mk n d)) :
C a

Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with rational numbers of the form n /. d with 0 < d and coprime n, d.

Equations
def rat.num_denom_cases_on' {C : Sort u} (a : ) (H : Π (n : ) (d : ), d 0C (rat.mk n d)) :
C a

Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with rational numbers of the form n /. d with d ≠ 0.

Equations
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
@[protected]

Addition of rational numbers. Use (+) instead.

Equations
@[protected, instance]
Equations
theorem rat.lift_binop_eq (f : ) (f₁ f₂ : ) (fv : ∀ {n₁ : } {d₁ : } {h₁ : 0 < d₁} {c₁ : n₁.nat_abs.coprime d₁} {n₂ : } {d₂ : } {h₂ : 0 < d₂} {c₂ : n₂.nat_abs.coprime d₂}, f {num := n₁, denom := d₁, pos := h₁, cop := c₁} {num := n₂, denom := d₂, pos := h₂, cop := c₂} = rat.mk (f₁ n₁ d₁ n₂ d₂) (f₂ n₁ d₁ n₂ d₂)) (f0 : ∀ {n₁ d₁ n₂ d₂ : }, d₁ 0d₂ 0f₂ n₁ d₁ n₂ d₂ 0) (a b c d : ) (b0 : b 0) (d0 : d 0) (H : ∀ {n₁ d₁ n₂ d₂ : }, a * d₁ = n₁ * bc * d₂ = n₂ * df₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂) :
f (rat.mk a b) (rat.mk c d) = rat.mk (f₁ a b c d) (f₂ a b c d)
@[simp]
theorem rat.add_def {a b c d : } (b0 : b 0) (d0 : d 0) :
b + d = rat.mk (a * d + c * b) (b * d)
@[protected]
def rat.neg (r : ) :

Negation of rational numbers. Use -r instead.

Equations
@[protected, instance]
def rat.has_neg  :
Equations
@[simp]
theorem rat.neg_def {a b : } :
- b = rat.mk (-a) b
@[simp]
theorem rat.mk_neg_denom (n d : ) :
(-d) = rat.mk (-n) d
@[protected]
def rat.mul  :

Multiplication of rational numbers. Use (*) instead.

Equations
@[protected, instance]
def rat.has_mul  :
Equations
@[simp]
theorem rat.mul_def {a b c d : } (b0 : b 0) (d0 : d 0) :
b * d = rat.mk (a * c) (b * d)
@[protected]
def rat.inv  :

Inverse rational number. Use r⁻¹ instead.

Equations
@[protected, instance]
def rat.has_inv  :
Equations
@[simp]
theorem rat.inv_def {a b : } :
(rat.mk a b)⁻¹ = a
@[protected]
theorem rat.add_zero (a : ) :
a + 0 = a
@[protected]
theorem rat.zero_add (a : ) :
0 + a = a
@[protected]
theorem rat.add_comm (a b : ) :
a + b = b + a
@[protected]
theorem rat.add_assoc (a b c : ) :
a + b + c = a + (b + c)
@[protected]
theorem rat.add_left_neg (a : ) :
-a + a = 0
@[simp]
theorem rat.mk_zero_one  :
1 = 0
@[simp]
theorem rat.mk_one_one  :
1 = 1
@[simp]
theorem rat.mk_neg_one_one  :
rat.mk (-1) 1 = -1
@[protected]
theorem rat.mul_one (a : ) :
a * 1 = a
@[protected]
theorem rat.one_mul (a : ) :
1 * a = a
@[protected]
theorem rat.mul_comm (a b : ) :
a * b = b * a
@[protected]
theorem rat.mul_assoc (a b c : ) :
a * b * c = a * (b * c)
@[protected]
theorem rat.add_mul (a b c : ) :
(a + b) * c = a * c + b * c
@[protected]
theorem rat.mul_add (a b c : ) :
a * (b + c) = a * b + a * c
@[protected]
theorem rat.zero_ne_one  :
0 1
@[protected]
theorem rat.mul_inv_cancel (a : ) :
a 0a * a⁻¹ = 1
@[protected]
theorem rat.inv_mul_cancel (a : ) (h : a 0) :
a⁻¹ * a = 1
@[protected, instance]
Equations
@[protected, instance]
def rat.field  :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def rat.monoid  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem rat.sub_def {a b c d : } (b0 : b 0) (d0 : d 0) :
b - d = rat.mk (a * d - c * b) (b * d)
@[simp]
theorem rat.denom_neg_eq_denom (q : ) :
(-q).denom = q.denom
@[simp]
theorem rat.num_neg_eq_neg_num (q : ) :
(-q).num = -q.num
@[simp]
theorem rat.num_zero  :
0.num = 0
@[simp]
theorem rat.denom_zero  :
0.denom = 1
theorem rat.zero_of_num_zero {q : } (hq : q.num = 0) :
q = 0
theorem rat.zero_iff_num_zero {q : } :
q = 0 q.num = 0
theorem rat.num_ne_zero_of_ne_zero {q : } (h : q 0) :
q.num 0
@[simp]
theorem rat.num_one  :
1.num = 1
@[simp]
theorem rat.denom_one  :
1.denom = 1
theorem rat.denom_ne_zero (q : ) :
theorem rat.eq_iff_mul_eq_mul {p q : } :
p = q p.num * (q.denom) = q.num * (p.denom)
theorem rat.mk_num_ne_zero_of_ne_zero {q : } {n d : } (hq : q 0) (hqnd : q = d) :
n 0
theorem rat.mk_denom_ne_zero_of_ne_zero {q : } {n d : } (hq : q 0) (hqnd : q = d) :
d 0
theorem rat.mk_ne_zero_of_ne_zero {n d : } (h : n 0) (hd : d 0) :
d 0
theorem rat.mul_num_denom (q r : ) :
q * r = rat.mk (q.num * r.num) (q.denom * r.denom)
theorem rat.div_num_denom (q r : ) :
q / r = rat.mk (q.num * (r.denom)) ((q.denom) * r.num)
theorem rat.num_denom_mk {q : } {n d : } (hd : d 0) (qdf : q = d) :
∃ (c : ), n = c * q.num d = c * (q.denom)
theorem rat.mk_pnat_num (n : ) (d : ℕ+) :
d).num = n / (n.nat_abs.gcd d)
theorem rat.mk_pnat_denom (n : ) (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 : ℕ+) :
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))
@[protected]
theorem rat.add_mk (a b c : ) :
rat.mk (a + b) c = c + c
theorem rat.coe_int_eq_mk (z : ) :
z = 1
theorem rat.mk_eq_div (n d : ) :
d = n / d
@[simp]
theorem rat.num_div_denom (r : ) :
(r.num) / (r.denom) = r
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.coe_int_eq_of_int (z : ) :
z =
@[simp, norm_cast]
theorem rat.coe_int_num (n : ) :
n.num = n
@[simp, norm_cast]
theorem rat.coe_int_denom (n : ) :
theorem rat.coe_int_num_of_denom_eq_one {q : } (hq : q.denom = 1) :
(q.num) = q
theorem rat.denom_eq_one_iff (r : ) :
r.denom = 1 (r.num) = r
@[protected, instance]
Equations
theorem rat.coe_nat_eq_mk (n : ) :
n = 1
@[simp, norm_cast]
theorem rat.coe_nat_num (n : ) :
@[simp, norm_cast]
theorem rat.coe_nat_denom (n : ) :
theorem rat.coe_int_inj (m n : ) :
m = n m = n
theorem rat.inv_def' {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 {a : } (ha0 : 0 < a) :
theorem rat.inv_coe_nat_num {a : } (ha0 : 0 < a) :
theorem rat.inv_coe_int_denom {a : } (ha0 : 0 < a) :
theorem rat.inv_coe_nat_denom {a : } (ha0 : 0 < 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)