mathlib documentation

data.rat.defs

Basics for the Rational Numbers #

Summary #

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

We then define the integral domain structure on and prove basic lemmas about it. The definition of the field structure on will be done in data.rat.basic once the field class has been defined.

Main Definitions #

Notations #

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]
@[protected, instance]
Equations
def rat.of_int (n : ) :

Embed an integer as a rational number

Equations
@[protected, instance]
Equations
@[protected, instance]
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
def rat.mk  :

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

Equations
theorem rat.mk_pnat_eq (n : ) (d : ) (h : 0 < d) :
rat.mk_pnat n d, h⟩ = rat.mk n d
theorem rat.mk_nat_eq (n : ) (d : ) :
@[simp]
theorem rat.mk_zero (n : ) :
rat.mk n 0 = 0
@[simp]
theorem rat.zero_mk_pnat (n : ℕ+) :
@[simp]
theorem rat.zero_mk_nat (n : ) :
@[simp]
theorem rat.zero_mk (n : ) :
rat.mk 0 n = 0
@[simp]
theorem rat.mk_eq_zero {a b : } (b0 : b 0) :
rat.mk a b = 0 a = 0
theorem rat.mk_ne_zero {a b : } (b0 : b 0) :
rat.mk a b 0 a 0
theorem rat.mk_eq {a b c d : } (hb : b 0) (hd : d 0) :
rat.mk a b = rat.mk c 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) = rat.mk a b
@[simp]
theorem rat.num_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} = rat.mk n d
theorem rat.of_int_eq_mk (z : ) :
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]
def rat.add  :

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) :
rat.mk a b + rat.mk c d = rat.mk (a * d + c * b) (b * d)
@[protected]
def rat.neg (r : ) :

Negation of rational numbers. Use -r instead.

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

Multiplication of rational numbers. Use (*) instead.

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

Inverse rational number. Use r⁻¹ instead.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem rat.inv_def {a b : } :
(rat.mk a b)⁻¹ = rat.mk 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  :
rat.mk 0 1 = 0
@[simp]
theorem rat.mk_one_one  :
rat.mk 1 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

At this point in the import hierarchy we have not defined the field typeclass. Instead we'll instantiate comm_ring and comm_group_with_zero at this point. The rat.field instance and any field-specific lemmas can be found in data.rat.basic.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem rat.sub_def {a b c d : } (b0 : b 0) (d0 : d 0) :
rat.mk a b - rat.mk c 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 = rat.mk n d) :
n 0
theorem rat.mk_denom_ne_zero_of_ne_zero {q : } {n d : } (hq : q 0) (hqnd : q = rat.mk n d) :
d 0
theorem rat.mk_ne_zero_of_ne_zero {n d : } (h : n 0) (hd : d 0) :
rat.mk n 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 = rat.mk n d) :
∃ (c : ), n = c * q.num d = c * (q.denom)
theorem rat.mk_pnat_num (n : ) (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 : ℕ+) :
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 = rat.mk a c + rat.mk b c
theorem rat.coe_int_eq_mk (z : ) :
z = rat.mk z 1
theorem rat.mk_eq_div (n d : ) :
rat.mk n d = n / d
theorem rat.mk_mul_mk_cancel {x : } (hx : x 0) (n d : ) :
rat.mk n x * rat.mk x d = rat.mk n d
theorem rat.mk_div_mk_cancel_left {x : } (hx : x 0) (n d : ) :
rat.mk n x / rat.mk d x = rat.mk n d
theorem rat.mk_div_mk_cancel_right {x : } (hx : x 0) (n d : ) :
rat.mk x n / rat.mk x d = rat.mk d n
theorem rat.coe_int_div_eq_mk {n d : } :
n / d = rat.mk 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.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)
@[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 : ) :
@[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)

Denominator as ℕ+ #

def rat.pnat_denom (x : ) :

Denominator as ℕ+.

Equations
@[simp]
theorem rat.coe_pnat_denom (x : ) :
@[simp]
theorem rat.pnat_denom_one  :
@[simp]
theorem rat.pnat_denom_zero  :