Euclidean domains #
This file introduces Euclidean domains and provides the extended Euclidean algorithm. To be precise,
a slightly more general version is provided which is sometimes called a transfinite Euclidean domain
and differs in the fact that the degree function need not take values in ℕ
but can take values in
any well-ordered set. Transfinite Euclidean domains were introduced by Motzkin and examples which
don't satisfy the classical notion were provided independently by Hiblot and Nagata.
Main definitions #
euclidean_domain
: Defines Euclidean domain with functionsquotient
andremainder
. Instances ofhas_div
andhas_mod
are provided, so that one can writea = b * (a / b) + a % b
.gcd
: defines the greatest common divisors of two elements of a Euclidean domain.xgcd
: given two elementsa b : R
,xgcd a b
defines the pair(x, y)
such thatx * a + y * b = gcd a b
.lcm
: defines the lowest common multiple of two elementsa
andb
of a Euclidean domain asa * b / (gcd a b)
Main statements #
gcd_eq_gcd_ab
: states Bézout's lemma for Euclidean domains.int.euclidean_domain
: shows thatℤ
is a Euclidean domain.field.to_euclidean_domain
: shows that any field is a Euclidean domain.
Notation #
≺
denotes the well founded relation on the Euclidean domain, e.g. in the example of the polynomial
ring over a field, p ≺ q
for polynomials p
and q
if and only if the degree of p
is less than
the degree of q
.
Implementation details #
Instead of working with a valuation, euclidean_domain
is implemented with the existence of a well
founded relation r
on the integral domain R
, which in the example of ℤ
would correspond to
setting i ≺ j
for integers i
and j
if the absolute value of i
is smaller than the absolute
value of j
.
References #
- Th. Motzkin, The Euclidean algorithm
- J.-J. Hiblot, Des anneaux euclidiens dont le plus petit algorithme n'est pas à valeurs finies
- M. Nagata, On Euclid algorithm
Tags #
Euclidean domain, transfinite Euclidean domain, Bézout's lemma
- to_comm_ring : comm_ring R
- to_nontrivial : nontrivial R
- quotient : R → R → R
- quotient_zero : ∀ (a : R), euclidean_domain.quotient a 0 = 0
- remainder : R → R → R
- quotient_mul_add_remainder_eq : ∀ (a b : R), b * euclidean_domain.quotient a b + euclidean_domain.remainder a b = a
- r : R → R → Prop
- r_well_founded : well_founded euclidean_domain.r
- remainder_lt : ∀ (a : R) {b : R}, b ≠ 0 → euclidean_domain.r (euclidean_domain.remainder a b) b
- mul_left_not_lt : ∀ (a : R) {b : R}, b ≠ 0 → ¬euclidean_domain.r (a * b) a
A euclidean_domain
is an non-trivial commutative ring with a division and a remainder,
satisfying b * (a / b) + a % b = a
.
The definition of a euclidean domain usually includes a valuation function R → ℕ
.
This definition is slightly generalised to include a well founded relation
r
with the property that r (a % b) b
, instead of a valuation.
Instances of this typeclass
Instances of other typeclasses for euclidean_domain
- euclidean_domain.has_sizeof_inst
Equations
- euclidean_domain.has_div = {div := euclidean_domain.quotient _inst_1}
Equations
- euclidean_domain.has_mod = {mod := euclidean_domain.remainder _inst_1}
gcd a b
is a (non-unique) element such that gcd a b ∣ a
gcd a b ∣ b
, and for
any element c
such that c ∣ a
and c ∣ b
, then c ∣ gcd a b
Equations
- euclidean_domain.gcd a = λ (b : R), ite (a = 0) b (euclidean_domain.gcd (b % a) a)
An implementation of the extended GCD algorithm.
At each step we are computing a triple (r, s, t)
, where r
is the next value of the GCD
algorithm, to compute the greatest common divisor of the input (say x
and y
), and s
and t
are the coefficients in front of x
and y
to obtain r
(i.e. r = s * x + t * y
).
The function xgcd_aux
takes in two triples, and from these recursively computes the next triple:
xgcd_aux (r, s, t) (r', s', t') = xgcd_aux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
Use the extended GCD algorithm to generate the a
and b
values
satisfying gcd x y = x * a + y * b
.
Equations
- euclidean_domain.xgcd x y = (euclidean_domain.xgcd_aux x 1 0 y 0 1).snd
The extended GCD a
value in the equation gcd x y = x * a + y * b
.
Equations
- euclidean_domain.gcd_a x y = (euclidean_domain.xgcd x y).fst
The extended GCD b
value in the equation gcd x y = x * a + y * b
.
Equations
- euclidean_domain.gcd_b x y = (euclidean_domain.xgcd x y).snd
An explicit version of Bézout's lemma for Euclidean domains.
lcm a b
is a (non-unique) element such that a ∣ lcm a b
b ∣ lcm a b
, and for
any element c
such that a ∣ c
and b ∣ c
, then lcm a b ∣ c
Equations
- euclidean_domain.lcm x y = x * y / euclidean_domain.gcd x y
Equations
- int.euclidean_domain = {to_comm_ring := {add := has_add.add int.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul int.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg int.has_neg, sub := comm_ring.sub int.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul int.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast int.comm_ring, nat_cast := comm_ring.nat_cast int.comm_ring, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul int.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow int.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}, to_nontrivial := int.euclidean_domain._proof_1, quotient := has_div.div int.has_div, quotient_zero := int.div_zero, remainder := has_mod.mod int.has_mod, quotient_mul_add_remainder_eq := int.euclidean_domain._proof_2, r := λ (a b : ℤ), a.nat_abs < b.nat_abs, r_well_founded := int.euclidean_domain._proof_3, remainder_lt := int.euclidean_domain._proof_4, mul_left_not_lt := int.euclidean_domain._proof_5}
Equations
- field.to_euclidean_domain = {to_comm_ring := {add := has_add.add (distrib.to_has_add K), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := field.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (sub_neg_monoid.to_has_neg K), sub := field.sub _inst_1, sub_eq_add_neg := _, zsmul := field.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := field.int_cast _inst_1, nat_cast := field.nat_cast _inst_1, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul (distrib.to_has_mul K), mul_assoc := _, one_mul := _, mul_one := _, npow := field.npow _inst_1, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}, to_nontrivial := _, quotient := has_div.div (div_inv_monoid.to_has_div K), quotient_zero := _, remainder := λ (a b : K), a - a * b / b, quotient_mul_add_remainder_eq := _, r := λ (a b : K), a = 0 ∧ b ≠ 0, r_well_founded := _, remainder_lt := _, mul_left_not_lt := _}