Basics for the Rational Numbers #
Summary #
We define a rational number q
as a structure { num, denom, pos, cop }
, where
num
is the numerator ofq
,denom
is the denominator ofq
,pos
is a proof thatdenom > 0
, andcop
is a proofnum
anddenom
are coprime.
We then 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 #
/.
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).
Instances for rat
- rat.smul_division_ring
- number_field.to_finite_dimensional
- rat.cast_coe
- rat.has_sizeof_inst
- rat.has_repr
- rat.has_to_string
- rat.has_to_format
- rat.encodable
- rat.has_zero
- rat.has_one
- rat.inhabited
- rat.has_add
- rat.has_neg
- rat.has_mul
- rat.has_inv
- rat.has_div
- rat.comm_ring
- rat.comm_group_with_zero
- rat.is_domain
- rat.nontrivial
- rat.comm_semiring
- rat.semiring
- rat.add_comm_group
- rat.add_group
- rat.add_comm_monoid
- rat.add_monoid
- rat.add_left_cancel_semigroup
- rat.add_right_cancel_semigroup
- rat.add_comm_semigroup
- rat.add_semigroup
- rat.comm_monoid
- rat.monoid
- rat.comm_semigroup
- rat.semigroup
- rat.int.can_lift
- rat.field
- rat.division_ring
- rat.has_le
- rat.linear_order
- rat.has_lt
- rat.distrib_lattice
- rat.lattice
- rat.semilattice_inf
- rat.semilattice_sup
- rat.has_inf
- rat.has_sup
- rat.partial_order
- rat.preorder
- rat.linear_ordered_field
- rat.linear_ordered_comm_ring
- rat.linear_ordered_ring
- rat.ordered_ring
- rat.linear_ordered_semiring
- rat.ordered_semiring
- rat.linear_ordered_add_comm_group
- rat.ordered_add_comm_group
- rat.ordered_cancel_add_comm_monoid
- rat.ordered_add_comm_monoid
- rat.reflect
- is_scalar_tower.rat
- smul_comm_class.rat
- smul_comm_class.rat'
- algebra_rat
- rat.is_fraction_ring
- self_adjoint.has_qsmul
- subfield_class.has_smul
- category_theory.functor.rat_linear
- rat.floor_ring
- rat.archimedean
- rat.metric_space
- rat.noncompact_space
- rat.uniform_add_group
- rat.topological_add_group
- rat.order_topology
- rat.topological_ring
- rat.normed_field
- rat.densely_normed_field
- normed_algebra_rat
- rat.normed_linear_ordered_field
- rat.measurable_space
- rat.measurable_singleton_class
- rat.borel_space
- rat.infinite
- rat.denumerable
- division_ring.has_continuous_const_smul_rat
- nnrat.rat.has_coe
- nnrat.can_lift
- nnrat.rat.algebra
- rat.number_field
- slim_check.rat.sampleable
- rat.totally_disconnected_space
Equations
- rat.has_repr = {repr := rat.repr}
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 := _}
Equations
- rat.has_zero = {zero := rat.of_int 0}
Equations
- rat.has_one = {one := rat.of_int 1}
Equations
- rat.inhabited = {default := 0}
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, _⟩)
Define a (dependent) function or prove ∀ r : ℚ, p r
by dealing with rational
numbers of the form n /. d
with d ≠ 0
.
Equations
- a.num_denom_cases_on' H = a.num_denom_cases_on (λ (n : ℤ) (d : ℕ) (h : 0 < d) (c : n.nat_abs.coprime d), H n d _)
Inverse rational number. Use r⁻¹
instead.
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 (λ (ᾰ : num = w_num), eq.rec (λ (w_cop : num.nat_abs.coprime w_denom), decidable.by_cases (λ (ᾰ : denom = w_denom), eq.rec (λ (w_pos : 0 < denom) (w_cop : num.nat_abs.coprime denom), decidable.is_true _) ᾰ w_pos w_cop) (λ (ᾰ : ¬denom = w_denom), decidable.is_false _)) ᾰ w_cop) (λ (ᾰ : ¬num = w_num), decidable.is_false _))))
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
.
Equations
- rat.comm_ring = {add := has_add.add rat.has_add, add_assoc := rat.add_assoc, zero := 0, zero_add := rat.zero_add, add_zero := rat.add_zero, nsmul := ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero, nsmul_zero' := rat.comm_ring._proof_1, nsmul_succ' := rat.comm_ring._proof_2, neg := has_neg.neg rat.has_neg, sub := ring.sub._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_3 rat.comm_ring._proof_4 has_neg.neg, sub_eq_add_neg := rat.comm_ring._proof_5, zsmul := ring.zsmul._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_6 rat.comm_ring._proof_7 has_neg.neg, zsmul_zero' := rat.comm_ring._proof_8, zsmul_succ' := rat.comm_ring._proof_9, zsmul_neg' := rat.comm_ring._proof_10, add_left_neg := rat.add_left_neg, add_comm := rat.add_comm, int_cast := ring.int_cast._default (λ (n : ℕ), rat.of_int ↑n) has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_11 rat.comm_ring._proof_12 1 rat.comm_ring._proof_13 rat.comm_ring._proof_14 has_neg.neg (ring.sub._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_3 rat.comm_ring._proof_4 has_neg.neg) rat.comm_ring._proof_15 (ring.zsmul._default has_add.add rat.add_assoc 0 rat.zero_add rat.add_zero (ring.nsmul._default 0 has_add.add rat.zero_add rat.add_zero) rat.comm_ring._proof_6 rat.comm_ring._proof_7 has_neg.neg) rat.comm_ring._proof_16 rat.comm_ring._proof_17 rat.comm_ring._proof_18 rat.add_left_neg, nat_cast := λ (n : ℕ), rat.of_int ↑n, one := 1, nat_cast_zero := rat.comm_ring._proof_19, nat_cast_succ := rat.comm_ring._proof_20, int_cast_of_nat := rat.comm_ring._proof_21, int_cast_neg_succ_of_nat := rat.comm_ring._proof_22, mul := has_mul.mul rat.has_mul, mul_assoc := rat.mul_assoc, one_mul := rat.one_mul, mul_one := rat.mul_one, npow := ring.npow._default 1 has_mul.mul rat.one_mul rat.mul_one, npow_zero' := rat.comm_ring._proof_23, npow_succ' := rat.comm_ring._proof_24, left_distrib := rat.mul_add, right_distrib := rat.add_mul, mul_comm := rat.mul_comm}
Equations
- rat.comm_group_with_zero = {mul := has_mul.mul rat.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := comm_ring.npow rat.comm_ring, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := 0, zero_mul := rat.comm_group_with_zero._proof_1, mul_zero := rat.comm_group_with_zero._proof_2, inv := has_inv.inv rat.has_inv, div := has_div.div rat.has_div, div_eq_mul_inv := rat.comm_group_with_zero._proof_3, zpow := group_with_zero.zpow._default has_mul.mul comm_ring.mul_assoc 1 comm_ring.one_mul comm_ring.mul_one comm_ring.npow comm_ring.npow_zero' comm_ring.npow_succ' has_inv.inv, zpow_zero' := rat.comm_group_with_zero._proof_4, zpow_succ' := rat.comm_group_with_zero._proof_5, zpow_neg' := rat.comm_group_with_zero._proof_6, exists_pair_ne := rat.comm_group_with_zero._proof_7, inv_zero := rat.comm_group_with_zero._proof_8, mul_inv_cancel := rat.mul_inv_cancel}