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 #
EuclideanDomain
: Defines Euclidean domain with functionsquotient
andremainder
. Instances ofDiv
andMod
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 #
See Algebra.EuclideanDomain.Basic
for most of the theorems about Euclidean domains,
including Bézout's lemma.
See Algebra.EuclideanDomain.Instances
for the fact that ℤ
is a Euclidean domain,
as is any field.
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, EuclideanDomain
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][MR32592]
- [J.-J. Hiblot, Des anneaux euclidiens dont le plus petit algorithme n'est pas à valeurs finies] [MR399081]
- [M. Nagata, On Euclid algorithm][MR541021]
Tags #
Euclidean domain, transfinite Euclidean domain, Bézout's lemma
A EuclideanDomain
is a 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.
- add : R → R → R
- zero : R
- nsmul : ℕ → R → R
- nsmul_zero : ∀ (x : R), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : R), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- mul : R → R → R
- one : R
- natCast : ℕ → R
- natCast_zero : NatCast.natCast 0 = 0
- natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
- npow : ℕ → R → R
- npow_zero : ∀ (x : R), Semiring.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : R), Semiring.npow (n + 1) x = Semiring.npow n x * x
- neg : R → R
- sub : R → R → R
- zsmul : ℤ → R → R
- zsmul_zero' : ∀ (a : R), Ring.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : R), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul (Int.ofNat n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : R), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
- intCast : ℤ → R
- intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
- intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
- exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
- quotient : R → R → R
A division function (denoted
/
) onR
. This satisfies the propertyb * (a / b) + a % b = a
, where%
denotesremainder
. - quotient_zero : ∀ (a : R), EuclideanDomain.quotient a 0 = 0
Division by zero should always give zero by convention.
- remainder : R → R → R
A remainder function (denoted
%
) onR
. This satisfies the propertyb * (a / b) + a % b = a
, where/
denotesquotient
. - quotient_mul_add_remainder_eq : ∀ (a b : R), b * EuclideanDomain.quotient a b + EuclideanDomain.remainder a b = a
The property that links the quotient and remainder functions. This allows us to compute GCDs and LCMs.
- r : R → R → Prop
A well-founded relation on
R
, satisfyingr (a % b) b
. This ensures that the GCD algorithm always terminates. - r_wellFounded : WellFounded EuclideanDomain.r
The relation
r
must be well-founded. This ensures that the GCD algorithm always terminates. - remainder_lt : ∀ (a : R) {b : R}, b ≠ 0 → EuclideanDomain.r (EuclideanDomain.remainder a b) b
- mul_left_not_lt : ∀ (a : R) {b : R}, b ≠ 0 → ¬EuclideanDomain.r (a * b) a
An additional constraint on
r
.
Instances
Division by zero should always give zero by convention.
The property that links the quotient and remainder functions. This allows us to compute GCDs and LCMs.
The relation r
must be well-founded.
This ensures that the GCD algorithm always terminates.
An additional constraint on r
.
Equations
- EuclideanDomain.wellFoundedRelation = { rel := EuclideanDomain.r, wf := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- EuclideanDomain.instDiv = { div := EuclideanDomain.quotient }
Equations
- EuclideanDomain.instMod = { mod := EuclideanDomain.remainder }
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
- EuclideanDomain.gcd a b = if a0 : a = 0 then b else let_fun x := ⋯; EuclideanDomain.gcd (b % a) a
Instances For
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 xgcdAux
takes in two triples, and from these recursively computes the next triple:
xgcdAux (r, s, t) (r', s', t') = xgcdAux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
Equations
- EuclideanDomain.xgcdAux r s t r' s' t' = if _hr : r = 0 then (r', s', t') else let q := r' / r; let_fun x := ⋯; EuclideanDomain.xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t
Instances For
Use the extended GCD algorithm to generate the a
and b
values
satisfying gcd x y = x * a + y * b
.
Equations
- EuclideanDomain.xgcd x y = (EuclideanDomain.xgcdAux x 1 0 y 0 1).2
Instances For
The extended GCD a
value in the equation gcd x y = x * a + y * b
.
Equations
- EuclideanDomain.gcdA x y = (EuclideanDomain.xgcd x y).1
Instances For
The extended GCD b
value in the equation gcd x y = x * a + y * b
.
Equations
- EuclideanDomain.gcdB x y = (EuclideanDomain.xgcd x y).2
Instances For
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
- EuclideanDomain.lcm x y = x * y / EuclideanDomain.gcd x y