Basics for the Rational Numbers
Summary
We define a rational number q as a structure { num, denom, pos, cop }, where
numis the numerator ofq,denomis the denominator ofq,posis a proof thatdenom > 0, andcopis a proofnumanddenomare coprime.
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
/.is infix notation forrat.mk.
Tags
rat, rationals, field, ℚ, numerator, denominator, num, denom
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).
Equations
Equations
- rat.encodable = encodable.of_equiv (Σ (n : ℤ), {d // 0 < d ∧ n.nat_abs.coprime d}) {to_fun := λ (_x : ℚ), rat.encodable._match_1 _x, inv_fun := λ (_x : Σ (n : ℤ), {d // 0 < d ∧ n.nat_abs.coprime d}), rat.encodable._match_2 _x, left_inv := rat.encodable._proof_1, right_inv := rat.encodable._proof_2}
- rat.encodable._match_1 {num := a, denom := b, pos := c, cop := d} = ⟨a, ⟨b, _⟩⟩
- rat.encodable._match_2 ⟨a, ⟨b, _⟩⟩ = {num := a, denom := b, pos := c, cop := d}
Embed an integer as a rational number
Equations
- rat.of_int n = {num := n, denom := 1, pos := nat.one_pos, cop := _}
Form the quotient n / d where n:ℤ and d:ℕ. In the case d = 0, we
define n / 0 = 0 by convention.
Equations
- rat.mk_nat n d = dite (d = 0) (λ (d0 : d = 0), 0) (λ (d0 : ¬d = 0), rat.mk_pnat n ⟨d, _⟩)
Equations
- rat.decidable_eq = id (λ (_v : ℚ), _v.cases_on (λ (num : ℤ) (denom : ℕ) (pos : 0 < denom) (cop : num.nat_abs.coprime denom) (w : ℚ), w.cases_on (λ (w_num : ℤ) (w_denom : ℕ) (w_pos : 0 < w_denom) (w_cop : w_num.nat_abs.coprime w_denom), decidable.by_cases (λ (a : num = w_num), eq.rec (λ (w_cop : num.nat_abs.coprime w_denom), decidable.by_cases (λ (a : denom = w_denom), eq.rec (λ (w_pos : 0 < denom) (w_cop : num.nat_abs.coprime denom), decidable.is_true _) a w_pos w_cop) (λ (a : ¬denom = w_denom), decidable.is_false _)) a w_cop) (λ (a : ¬num = w_num), decidable.is_false _))))
Equations
- rat.field = {add := rat.add, add_assoc := rat.add_assoc, zero := 0, zero_add := rat.zero_add, add_zero := rat.add_zero, neg := rat.neg, add_left_neg := rat.add_left_neg, add_comm := rat.add_comm, mul := rat.mul, mul_assoc := rat.mul_assoc, one := 1, one_mul := rat.one_mul, mul_one := rat.mul_one, left_distrib := rat.mul_add, right_distrib := rat.add_mul, mul_comm := rat.mul_comm, inv := rat.inv, exists_pair_ne := rat.field._proof_1, mul_inv_cancel := rat.mul_inv_cancel, inv_zero := rat.field._proof_2}