mathlib documentation

data.rat.defs

Basics for the Rational Numbers #

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 #

Notations #

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 : ) :
@[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]
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
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.coe_int_eq_mk (z : ) :
z = rat.mk 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]
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₁ 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) :
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 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
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) :
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.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)
@[protected]
theorem rat.add_mk (a b c : ) :
rat.mk (a + b) c = rat.mk a c + rat.mk b c
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.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  :
can_lift coe (λ (q : ), q.denom = 1)
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