mathlib3 documentation

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 #

Notations #

source
def rat.of_int (n : ℤ) :
ℚ

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

Equations
source
@[protected, instance]
def rat.has_int_cast  :
has_int_cast ℚ
Equations
source
@[simp]
theorem rat.of_int_eq_cast (n : ℤ) :
rat.of_int n = ↑n
source
@[simp, norm_cast]
theorem rat.coe_int_num (n : ℤ) :
↑n.num = n
source
@[simp, norm_cast]
theorem rat.coe_int_denom (n : ℤ) :
↑n.denom = 1
source
@[protected, instance]
def rat.has_zero  :
has_zero ℚ
Equations
source
@[protected, instance]
def rat.has_one  :
has_one ℚ
Equations
source
@[protected, instance]
def rat.inhabited  :
inhabited ℚ
Equations
source
def rat.mk_pnat (n : ℤ) :
ℕ+ → ℚ

Form the quotient n / d where n:ℤ and d:ℕ+ (not necessarily coprime)

Equations
source
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
source
def rat.mk  :
ℤ → ℤ → ℚ

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

Equations
source
theorem rat.mk_pnat_eq (n : ℤ) (d : ℕ) (h : 0 < d) :
rat.mk_pnat n ⟨d, h⟩ = rat.mk n ↑d
source
theorem rat.mk_nat_eq (n : ℤ) (d : ℕ) :
rat.mk_nat n d = rat.mk n ↑d
source
@[simp]
theorem rat.mk_zero (n : ℤ) :
rat.mk n 0 = 0
source
@[simp]
theorem rat.zero_mk_pnat (n : ℕ+) :
rat.mk_pnat 0 n = 0
source
@[simp]
theorem rat.zero_mk_nat (n : ℕ) :
rat.mk_nat 0 n = 0
source
@[simp]
theorem rat.zero_mk (n : ℤ) :
rat.mk 0 n = 0
source
@[simp]
theorem rat.mk_eq_zero {a b : ℤ} (b0 : b ≠ 0) :
rat.mk a b = 0 ↔ a = 0
source
theorem rat.mk_ne_zero {a b : ℤ} (b0 : b ≠ 0) :
rat.mk a b ≠ 0 ↔ a ≠ 0
source
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
source
@[simp]
theorem rat.div_mk_div_cancel_left {a b c : ℤ} (c0 : c ≠ 0) :
rat.mk (a * c) (b * c) = rat.mk a b
source
@[simp]
theorem rat.num_denom {a : ℚ} :
rat.mk a.num ↑(a.denom) = a
source
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
source
theorem rat.coe_int_eq_mk (z : ℤ) :
↑z = rat.mk z 1
source
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
source
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
source
@[protected]
def rat.add  :
ℚ → ℚ → ℚ

Addition of rational numbers. Use (+) instead.

Equations
source
@[protected, instance]
def rat.has_add  :
has_add ℚ
Equations
source
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)
source
@[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)
source
@[protected]
def rat.neg (r : ℚ) :
ℚ

Negation of rational numbers. Use -r instead.

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

Multiplication of rational numbers. Use (*) instead.

Equations
source
@[protected, instance]
def rat.has_mul  :
has_mul ℚ
Equations
source
@[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)
source
@[protected]
def rat.inv  :
ℚ → ℚ

Inverse rational number. Use r⁻¹ instead.

Equations
source
@[protected, instance]
def rat.has_inv  :
has_inv ℚ
Equations
source
@[protected, instance]
def rat.has_div  :
has_div ℚ
Equations
source
@[simp]
theorem rat.inv_def {a b : ℤ} :
(rat.mk a b)⁻¹ = rat.mk b a
source
@[protected]
theorem rat.add_zero (a : ℚ) :
a + 0 = a
source
@[protected]
theorem rat.zero_add (a : ℚ) :
0 + a = a
source
@[protected]
theorem rat.add_comm (a b : ℚ) :
a + b = b + a
source
@[protected]
theorem rat.add_assoc (a b c : ℚ) :
a + b + c = a + (b + c)
source
@[protected]
theorem rat.add_left_neg (a : ℚ) :
-a + a = 0
source
@[simp]
theorem rat.mk_zero_one  :
rat.mk 0 1 = 0
source
@[simp]
theorem rat.mk_one_one  :
rat.mk 1 1 = 1
source
@[simp]
theorem rat.mk_neg_one_one  :
rat.mk (-1) 1 = -1
source
@[protected]
theorem rat.mul_one (a : ℚ) :
a * 1 = a
source
@[protected]
theorem rat.one_mul (a : ℚ) :
1 * a = a
source
@[protected]
theorem rat.mul_comm (a b : ℚ) :
a * b = b * a
source
@[protected]
theorem rat.mul_assoc (a b c : ℚ) :
a * b * c = a * (b * c)
source
@[protected]
theorem rat.add_mul (a b c : ℚ) :
(a + b) * c = a * c + b * c
source
@[protected]
theorem rat.mul_add (a b c : ℚ) :
a * (b + c) = a * b + a * c
source
@[protected]
theorem rat.zero_ne_one  :
0 ≠ 1
source
@[protected]
theorem rat.mul_inv_cancel (a : ℚ) :
a ≠ 0 → a * a⁻¹ = 1
source
@[protected]
theorem rat.inv_mul_cancel (a : ℚ) (h : a ≠ 0) :
a⁻¹ * a = 1
source
@[protected, instance]
def rat.decidable_eq  :
decidable_eq ℚ
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.

source
@[protected, instance]
def rat.comm_ring  :
comm_ring ℚ
Equations
source
@[protected, instance]
def rat.comm_group_with_zero  :
comm_group_with_zero ℚ
Equations
source
@[protected, instance]
def rat.is_domain  :
is_domain ℚ
source
@[protected, instance]
def rat.nontrivial  :
nontrivial ℚ
source
@[protected, instance]
def rat.comm_semiring  :
comm_semiring ℚ
Equations
source
@[protected, instance]
def rat.semiring  :
semiring ℚ
Equations
source
@[protected, instance]
def rat.add_comm_group  :
add_comm_group ℚ
Equations
source
@[protected, instance]
def rat.add_group  :
add_group ℚ
Equations
source
@[protected, instance]
def rat.add_comm_monoid  :
add_comm_monoid ℚ
Equations
source
@[protected, instance]
def rat.add_monoid  :
add_monoid ℚ
Equations
source
@[protected, instance]
def rat.add_left_cancel_semigroup  :
add_left_cancel_semigroup ℚ
Equations
source
@[protected, instance]
def rat.add_right_cancel_semigroup  :
add_right_cancel_semigroup ℚ
Equations
source
@[protected, instance]
def rat.add_comm_semigroup  :
add_comm_semigroup ℚ
Equations
source
@[protected, instance]
def rat.add_semigroup  :
add_semigroup ℚ
Equations
source
@[protected, instance]
def rat.comm_monoid  :
comm_monoid ℚ
Equations
source
@[protected, instance]
def rat.monoid  :
monoid ℚ
Equations
source
@[protected, instance]
def rat.comm_semigroup  :
comm_semigroup ℚ
Equations
source
@[protected, instance]
def rat.semigroup  :
semigroup ℚ
Equations
source
theorem rat.denom_ne_zero (q : ℚ) :
q.denom ≠ 0
source
theorem rat.eq_iff_mul_eq_mul {p q : ℚ} :
p = q ↔ p.num * ↑(q.denom) = q.num * ↑(p.denom)
source
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)
source
@[simp]
theorem rat.denom_neg_eq_denom (q : ℚ) :
(-q).denom = q.denom
source
@[simp]
theorem rat.num_neg_eq_neg_num (q : ℚ) :
(-q).num = -q.num
source
@[simp]
theorem rat.num_zero  :
0.num = 0
source
@[simp]
theorem rat.denom_zero  :
0.denom = 1
source
theorem rat.zero_of_num_zero {q : ℚ} (hq : q.num = 0) :
q = 0
source
theorem rat.zero_iff_num_zero {q : ℚ} :
q = 0 ↔ q.num = 0
source
theorem rat.num_ne_zero_of_ne_zero {q : ℚ} (h : q ≠ 0) :
q.num ≠ 0
source
@[simp]
theorem rat.num_one  :
1.num = 1
source
@[simp]
theorem rat.denom_one  :
1.denom = 1
source
theorem rat.mk_num_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = rat.mk n d) :
n ≠ 0
source
theorem rat.mk_denom_ne_zero_of_ne_zero {q : ℚ} {n d : ℤ} (hq : q ≠ 0) (hqnd : q = rat.mk n d) :
d ≠ 0
source
theorem rat.mk_ne_zero_of_ne_zero {n d : ℤ} (h : n ≠ 0) (hd : d ≠ 0) :
rat.mk n d ≠ 0
source
theorem rat.mul_num_denom (q r : ℚ) :
q * r = rat.mk (q.num * r.num) ↑(q.denom * r.denom)
source
theorem rat.div_num_denom (q r : ℚ) :
q / r = rat.mk (q.num * ↑(r.denom)) (↑(q.denom) * r.num)
source
@[protected]
theorem rat.add_mk (a b c : ℤ) :
rat.mk (a + b) c = rat.mk a c + rat.mk b c
source
theorem rat.mk_eq_div (n d : ℤ) :
rat.mk n d = ↑n / ↑d
source
theorem rat.mk_mul_mk_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
rat.mk n x * rat.mk x d = rat.mk n d
source
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
source
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
source
theorem rat.coe_int_div_eq_mk {n d : ℤ} :
↑n / ↑d = rat.mk n d
source
@[simp]
theorem rat.num_div_denom (r : ℚ) :
↑(r.num) / ↑(r.denom) = r
source
theorem rat.coe_int_num_of_denom_eq_one {q : ℚ} (hq : q.denom = 1) :
↑(q.num) = q
source
theorem rat.denom_eq_one_iff (r : ℚ) :
r.denom = 1 ↔ ↑(r.num) = r
source
@[protected, instance]
def rat.can_lift  :
can_lift ℚ ℤ coe (λ (q : ℚ), q.denom = 1)
Equations
source
theorem rat.coe_nat_eq_mk (n : ℕ) :
↑n = rat.mk ↑n 1
source
@[simp, norm_cast]
theorem rat.coe_nat_num (n : ℕ) :
↑n.num = ↑n
source
@[simp, norm_cast]
theorem rat.coe_nat_denom (n : ℕ) :
↑n.denom = 1
source
theorem rat.coe_int_inj (m n : ℤ) :
↑m = ↑n ↔ m = n