mathlib documentation

data.rat.basic

Basics for the Rational Numbers #

Summary #

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

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 #

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).

def rat.repr  :

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

Equations
@[instance]
Equations
@[instance]
@[instance]
Equations
def rat.of_int (n : ) :

Embed an integer as a rational number

Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
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⟩ = n /. d
theorem rat.mk_nat_eq (n : ) (d : ) :
@[simp]
theorem rat.mk_zero (n : ) :
n /. 0 = 0
@[simp]
theorem rat.zero_mk_pnat (n : ℕ+) :
@[simp]
theorem rat.zero_mk_nat (n : ) :
@[simp]
theorem rat.zero_mk (n : ) :
0 /. n = 0
@[simp]
theorem rat.mk_eq_zero {a b : } (b0 : b 0) :
a /. b = 0 a = 0
theorem rat.mk_eq {a b c d : } (hb : b 0) (hd : d 0) :
a /. b = c /. d a * d = c * b
@[simp]
theorem rat.div_mk_div_cancel_left {a b c : } (c0 : c 0) :
a * c /. b * c = a /. b
@[simp]
theorem rat.num_denom {a : } :
a.num /. (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} = 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 (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 (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) :
(a /. b).num a
theorem rat.denom_dvd (a b : ) :
((a /. b).denom) b
def rat.add  :

Addition of rational numbers. Use (+) instead.

Equations
@[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₂} = 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₂ * d(f₁ n₁ d₁ n₂ d₂) * f₂ a b c d = (f₁ a b c d) * f₂ n₁ d₁ n₂ d₂) :
f (a /. b) (c /. d) = 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) :
a /. b + c /. d = (a * d + c * b) /. b * d
def rat.neg (r : ) :

Negation of rational numbers. Use -r instead.

Equations
@[instance]
Equations
@[simp]
theorem rat.neg_def {a b : } :
-(a /. b) = -a /. b
def rat.mul  :

Multiplication of rational numbers. Use (*) instead.

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

Inverse rational number. Use r⁻¹ instead.

Equations
@[instance]
Equations
@[simp]
theorem rat.inv_def {a b : } :
(a /. b)⁻¹ = b /. a
theorem rat.add_zero (a : ) :
a + 0 = a
theorem rat.zero_add (a : ) :
0 + a = a
theorem rat.add_comm (a b : ) :
a + b = b + a
theorem rat.add_assoc (a b c : ) :
a + b + c = a + (b + c)
theorem rat.add_left_neg (a : ) :
-a + a = 0
@[simp]
theorem rat.mk_zero_one  :
0 /. 1 = 0
@[simp]
theorem rat.mk_one_one  :
1 /. 1 = 1
@[simp]
theorem rat.mk_neg_one_one  :
(-1) /. 1 = -1
theorem rat.mul_one (a : ) :
a * 1 = a
theorem rat.one_mul (a : ) :
1 * a = a
theorem rat.mul_comm (a b : ) :
a * b = b * a
theorem rat.mul_assoc (a b c : ) :
(a * b) * c = a * b * c
theorem rat.add_mul (a b c : ) :
(a + b) * c = a * c + b * c
theorem rat.mul_add (a b c : ) :
a * (b + c) = a * b + a * c
theorem rat.zero_ne_one  :
0 1
theorem rat.mul_inv_cancel (a : ) :
a 0a * a⁻¹ = 1
theorem rat.inv_mul_cancel (a : ) (h : a 0) :
a⁻¹ * a = 1
@[instance]
Equations
@[instance]
def rat.field  :
Equations
@[instance]
@[instance]
Equations
theorem rat.sub_def {a b c d : } (b0 : b 0) (d0 : d 0) :
a /. b - c /. d = (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 = n /. d) :
n 0
theorem rat.mk_denom_ne_zero_of_ne_zero {q : } {n d : } (hq : q 0) (hqnd : q = n /. d) :
d 0
theorem rat.mk_ne_zero_of_ne_zero {n d : } (h : n 0) (hd : d 0) :
n /. d 0
theorem rat.mul_num_denom (q r : ) :
q * r = (q.num) * r.num /. (q.denom) * r.denom
theorem rat.div_num_denom (q r : ) :
q / r = (q.num) * (r.denom) /. ((q.denom)) * r.num
theorem rat.num_denom_mk {q : } {n d : } (hn : n 0) (hd : d 0) (qdf : q = 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.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 = ((q.num) * (r.denom) + ((q.denom)) * r.num) /. ((q.denom)) * (r.denom)
theorem rat.add_mk (a b c : ) :
(a + b) /. c = a /. c + b /. c
theorem rat.coe_int_eq_mk (z : ) :
z = z /. 1
theorem rat.mk_eq_div (n d : ) :
n /. 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 : } (n_ne_zero : n 0) (d_ne_zero : d 0) :
∃ (c : ), n = c * (n / d).num d = c * ((n / d).denom)
@[simp]
theorem rat.coe_int_num (n : ) :
n.num = n
@[simp]
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
@[instance]
Equations
theorem rat.coe_nat_eq_mk (n : ) :
n = n /. 1
@[simp]
theorem rat.coe_nat_num (n : ) :
@[simp]
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
theorem rat.coe_int_div_self (n : ) :
(n / n) = n / n
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.forall {p : → Prop} :
(∀ (r : ), p r) ∀ (a b : ), p (a / b)
theorem rat.exists {p : → Prop} :
(∃ (r : ), p r) ∃ (a b : ), p (a / b)