# mathlib3documentation

algebra.euclidean_domain.defs

# Euclidean domains #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 functions quotient and remainder. Instances of has_div and has_mod are provided, so that one can write a = b * (a / b) + a % b.
• gcd: defines the greatest common divisors of two elements of a Euclidean domain.
• xgcd: given two elements a b : R, xgcd a b defines the pair (x, y) such that x * a + y * b = gcd a b.
• lcm: defines the lowest common multiple of two elements a and b of a Euclidean domain as a * b / (gcd a b)

## Main statements #

See algebra.euclidean_domain.basic for most of the theorems about Euclidean domains, including Bézout's lemma.

See algebra.euclidean_domain.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, 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.

## Tags #

Euclidean domain, transfinite Euclidean domain, Bézout's lemma

@[class]
structure euclidean_domain (R : Type u) :
• to_comm_ring :
• to_nontrivial :
• quotient : R R R
• quotient_zero : (a : R),
• remainder : R R R
• quotient_mul_add_remainder_eq : (a b : R), = a
• r : R R Prop
• r_well_founded :
• remainder_lt : (a : R) {b : R}, b 0
• 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
@[protected, instance]
def euclidean_domain.has_div {R : Type u}  :
Equations
@[protected, instance]
def euclidean_domain.has_mod {R : Type u}  :
Equations
theorem euclidean_domain.div_add_mod {R : Type u} (a b : R) :
b * (a / b) + a % b = a
theorem euclidean_domain.mod_add_div {R : Type u} (a b : R) :
a % b + b * (a / b) = a
theorem euclidean_domain.mod_add_div' {R : Type u} (m k : R) :
m % k + m / k * k = m
theorem euclidean_domain.div_add_mod' {R : Type u} (m k : R) :
m / k * k + m % k = m
theorem euclidean_domain.mod_eq_sub_mul_div {R : Type u_1} (a b : R) :
a % b = a - b * (a / b)
theorem euclidean_domain.mod_lt {R : Type u} (a : R) {b : R} :
theorem euclidean_domain.mul_right_not_lt {R : Type u} {a : R} (b : R) (h : a 0) :
@[simp]
theorem euclidean_domain.mod_zero {R : Type u} (a : R) :
a % 0 = a
theorem euclidean_domain.lt_one {R : Type u} (a : R) :
a = 0
theorem euclidean_domain.val_dvd_le {R : Type u} (a b : R) :
b a a 0
@[simp]
theorem euclidean_domain.div_zero {R : Type u} (a : R) :
a / 0 = 0
theorem euclidean_domain.gcd.induction {R : Type u} {P : R R Prop} (a b : R) :
( (x : R), P 0 x) ( (a b : R), a 0 P (b % a) a P a b) P a b
def euclidean_domain.gcd {R : Type u} [decidable_eq R] :
R R R

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
@[simp]
theorem euclidean_domain.gcd_zero_left {R : Type u} [decidable_eq R] (a : R) :
def euclidean_domain.xgcd_aux {R : Type u} [decidable_eq R] :
R R R R R R R × R × R

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)

Equations
@[simp]
theorem euclidean_domain.xgcd_zero_left {R : Type u} [decidable_eq R] {s t r' s' t' : R} :
r' s' t' = (r', s', t')
theorem euclidean_domain.xgcd_aux_rec {R : Type u} [decidable_eq R] {r s t r' s' t' : R} (h : r 0) :
r' s' t' = euclidean_domain.xgcd_aux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
def euclidean_domain.xgcd {R : Type u} [decidable_eq R] (x y : R) :
R × R

Use the extended GCD algorithm to generate the a and b values satisfying gcd x y = x * a + y * b.

Equations
def euclidean_domain.gcd_a {R : Type u} [decidable_eq R] (x y : R) :
R

The extended GCD a value in the equation gcd x y = x * a + y * b.

Equations
def euclidean_domain.gcd_b {R : Type u} [decidable_eq R] (x y : R) :
R

The extended GCD b value in the equation gcd x y = x * a + y * b.

Equations
@[simp]
theorem euclidean_domain.gcd_a_zero_left {R : Type u} [decidable_eq R] {s : R} :
@[simp]
theorem euclidean_domain.gcd_b_zero_left {R : Type u} [decidable_eq R] {s : R} :
theorem euclidean_domain.xgcd_val {R : Type u} [decidable_eq R] (x y : R) :
def euclidean_domain.lcm {R : Type u} [decidable_eq R] (x y : R) :
R

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