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 (a : ) :

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 : ) (a : ℕ+) :

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 (a a_1 : ) :

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

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

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 (a a_1 : ) :

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 (a : ) :

Equations
@[instance]

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

def rat.mul (a a_1 : ) :

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 (a : ) :

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

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_1 : a 0) :
a * a⁻¹ = 1

theorem rat.inv_mul_cancel (a : ) (h : a 0) :
a⁻¹ * a = 1

@[instance]

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

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.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.coe_int_eq_mk (z : ) :
z = z /. 1

theorem rat.mk_eq_div (n d : ) :
n /. d = n / d

@[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

@[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)