data.rat.defs

# Basics for the Rational Numbers #

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

## Summary #

We 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 #

• rat.mk n d constructs a rational number q = n / d from n d : ℤ.

## Notations #

• /. is infix notation for rat.mk.
def rat.of_int (n : ) :

Embed an integer as a rational number. You should use the coercion coe : ℤ → ℚ instead.

Equations
@[protected, instance]
Equations
@[simp]
theorem rat.of_int_eq_cast (n : ) :
= n
@[simp, norm_cast]
theorem rat.coe_int_num (n : ) :
n.num = n
@[simp, norm_cast]
theorem rat.coe_int_denom (n : ) :
@[protected, instance]
Equations
@[protected, instance]
def rat.has_one  :
Equations
@[protected, 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
• 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.coe_int_eq_mk (z : ) :
z = 1
def rat.num_denom_cases_on {C : Sort u} (a : ) (H : Π (n : ) (d : ), 0 < d n.nat_abs.coprime d C (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 0 C (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
@[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₁ 0 d₂ 0 f₂ n₁ d₁ n₂ d₂ 0) (a b c d : ) (b0 : b 0) (d0 : d 0) (H : {n₁ d₁ n₂ d₂ : }, a * d₁ = n₁ * b c * d₂ = n₂ * d f₁ 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
@[protected, instance]
def rat.has_div  :
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 0 a * 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
@[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.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.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.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)
@[protected]
theorem rat.add_mk (a b c : ) :
rat.mk (a + b) c = c + c
theorem rat.mk_eq_div (n d : ) :
d = n / d
theorem rat.mk_mul_mk_cancel {x : } (hx : x 0) (n d : ) :
x * d = d
theorem rat.mk_div_mk_cancel_left {x : } (hx : x 0) (n d : ) :
x / x = d
theorem rat.mk_div_mk_cancel_right {x : } (hx : x 0) (n d : ) :
n / d = n
theorem rat.coe_int_div_eq_mk {n d : } :
n / d = d
@[simp]
theorem rat.num_div_denom (r : ) :
(r.num) / (r.denom) = r
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]
def rat.can_lift  :
(λ (q : ), q.denom = 1)
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