mathlib documentation

algebra.euclidean_domain

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 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 #

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 #

Tags #

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

@[class]

structure euclidean_domain (R : Type u) :

Type u

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

@[protected, instance]

def euclidean_domain.has_div {R : Type u} [euclidean_domain R] :

Equations

euclidean_domain.has_div = {div := euclidean_domain.quotient _inst_1}

@[protected, instance]

def euclidean_domain.has_mod {R : Type u} [euclidean_domain R] :

Equations

euclidean_domain.has_mod = {mod := euclidean_domain.remainder _inst_1}

theorem euclidean_domain.div_add_mod {R : Type u} [euclidean_domain R] (a b : R) :

b * (a / b) + a % b = a

theorem euclidean_domain.mod_add_div {R : Type u} [euclidean_domain R] (a b : R) :

a % b + b * (a / b) = a

theorem euclidean_domain.mod_add_div' {R : Type u} [euclidean_domain R] (m k : R) :

m % k + (m / k) * k = m

theorem euclidean_domain.div_add_mod' {R : Type u} [euclidean_domain R] (m k : R) :

(m / k) * k + m % k = m

theorem euclidean_domain.mod_eq_sub_mul_div {R : Type u_1} [euclidean_domain R] (a b : R) :

a % b = a - b * (a / b)

theorem euclidean_domain.mod_lt {R : Type u} [euclidean_domain R] (a : R) {b : R} :

b ≠ 0 → euclidean_domain.r (a % b) b

theorem euclidean_domain.mul_right_not_lt {R : Type u} [euclidean_domain R] {a : R} (b : R) (h : a ≠ 0) :

¬euclidean_domain.r (a * b) b

theorem euclidean_domain.mul_div_cancel_left {R : Type u} [euclidean_domain R] {a : R} (b : R) (a0 : a ≠ 0) :

a * b / a = b

theorem euclidean_domain.mul_div_cancel {R : Type u} [euclidean_domain R] (a : R) {b : R} (b0 : b ≠ 0) :

a * b / b = a

@[simp]

theorem euclidean_domain.mod_zero {R : Type u} [euclidean_domain R] (a : R) :

a % 0 = a

@[simp]

theorem euclidean_domain.mod_eq_zero {R : Type u} [euclidean_domain R] {a b : R} :

a % b = 0 ↔ b ∣ a

@[simp]

theorem euclidean_domain.mod_self {R : Type u} [euclidean_domain R] (a : R) :

a % a = 0

theorem euclidean_domain.dvd_mod_iff {R : Type u} [euclidean_domain R] {a b c : R} (h : c ∣ b) :

c ∣ a % b ↔ c ∣ a

theorem euclidean_domain.lt_one {R : Type u} [euclidean_domain R] (a : R) :

euclidean_domain.r a 1 → a = 0

theorem euclidean_domain.val_dvd_le {R : Type u} [euclidean_domain R] (a b : R) :

b ∣ a → a ≠ 0 → ¬euclidean_domain.r a b

@[simp]

theorem euclidean_domain.mod_one {R : Type u} [euclidean_domain R] (a : R) :

a % 1 = 0

@[simp]

theorem euclidean_domain.zero_mod {R : Type u} [euclidean_domain R] (b : R) :

0 % b = 0

@[simp]

theorem euclidean_domain.div_zero {R : Type u} [euclidean_domain R] (a : R) :

a / 0 = 0

@[simp]

theorem euclidean_domain.zero_div {R : Type u} [euclidean_domain R] {a : R} :

0 / a = 0

@[simp]

theorem euclidean_domain.div_self {R : Type u} [euclidean_domain R] {a : R} (a0 : a ≠ 0) :

a / a = 1

theorem euclidean_domain.eq_div_of_mul_eq_left {R : Type u} [euclidean_domain R] {a b c : R} (hb : b ≠ 0) (h : a * b = c) :

a = c / b

theorem euclidean_domain.eq_div_of_mul_eq_right {R : Type u} [euclidean_domain R] {a b c : R} (ha : a ≠ 0) (h : a * b = c) :

b = c / a

theorem euclidean_domain.mul_div_assoc {R : Type u} [euclidean_domain R] (x : R) {y z : R} (h : z ∣ y) :

x * y / z = x * (y / z)

@[simp]

theorem euclidean_domain.div_one {R : Type u} [euclidean_domain R] (p : R) :

p / 1 = p

theorem euclidean_domain.div_dvd_of_dvd {R : Type u} [euclidean_domain R] {p q : R} (hpq : q ∣ p) :

p / q ∣ p

theorem euclidean_domain.gcd.induction {R : Type u} [euclidean_domain R] {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} [euclidean_domain R] [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

euclidean_domain.gcd a = λ (b : R), ite (a = 0) b (euclidean_domain.gcd (b % a) a)

@[simp]

theorem euclidean_domain.gcd_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :

euclidean_domain.gcd 0 a = a

@[simp]

theorem euclidean_domain.gcd_zero_right {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :

euclidean_domain.gcd a 0 = a

theorem euclidean_domain.gcd_val {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :

euclidean_domain.gcd a b = euclidean_domain.gcd (b % a) a

theorem euclidean_domain.gcd_dvd {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :

euclidean_domain.gcd a b ∣ a ∧ euclidean_domain.gcd a b ∣ b

theorem euclidean_domain.gcd_dvd_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :

euclidean_domain.gcd a b ∣ a

theorem euclidean_domain.gcd_dvd_right {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :

euclidean_domain.gcd a b ∣ b

@[protected]

theorem euclidean_domain.gcd_eq_zero_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {a b : R} :

euclidean_domain.gcd a b = 0 ↔ a = 0 ∧ b = 0

theorem euclidean_domain.dvd_gcd {R : Type u} [euclidean_domain R] [decidable_eq R] {a b c : R} :

c ∣ a → c ∣ b → c ∣ euclidean_domain.gcd a b

theorem euclidean_domain.gcd_eq_left {R : Type u} [euclidean_domain R] [decidable_eq R] {a b : R} :

euclidean_domain.gcd a b = a ↔ a ∣ b

@[simp]

theorem euclidean_domain.gcd_one_left {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :

euclidean_domain.gcd 1 a = 1

@[simp]

theorem euclidean_domain.gcd_self {R : Type u} [euclidean_domain R] [decidable_eq R] (a : R) :

euclidean_domain.gcd a a = a

def euclidean_domain.xgcd_aux {R : Type u} [euclidean_domain R] [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

euclidean_domain.xgcd_aux r = λ (s t r' s' t' : R), ite (r = 0) (r', s', t') (let q : R := r' / r in euclidean_domain.xgcd_aux (r' % r) (s' - q * s) (t' - q * t) r s t)

@[simp]

theorem euclidean_domain.xgcd_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] {s t r' s' t' : R} :

euclidean_domain.xgcd_aux 0 s t r' s' t' = (r', s', t')

theorem euclidean_domain.xgcd_aux_rec {R : Type u} [euclidean_domain R] [decidable_eq R] {r s t r' s' t' : R} (h : r ≠ 0) :

euclidean_domain.xgcd_aux r s t 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} [euclidean_domain R] [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

euclidean_domain.xgcd x y = (euclidean_domain.xgcd_aux x 1 0 y 0 1).snd

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

R

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

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

R

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

@[simp]

theorem euclidean_domain.gcd_a_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] {s : R} :

euclidean_domain.gcd_a 0 s = 0

@[simp]

theorem euclidean_domain.gcd_b_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] {s : R} :

euclidean_domain.gcd_b 0 s = 1

@[simp]

theorem euclidean_domain.xgcd_aux_fst {R : Type u} [euclidean_domain R] [decidable_eq R] (x y s t s' t' : R) :

(euclidean_domain.xgcd_aux x s t y s' t').fst = euclidean_domain.gcd x y

theorem euclidean_domain.xgcd_aux_val {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :

euclidean_domain.xgcd_aux x 1 0 y 0 1 = (euclidean_domain.gcd x y, euclidean_domain.xgcd x y)

theorem euclidean_domain.xgcd_val {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :

euclidean_domain.xgcd x y = (euclidean_domain.gcd_a x y, euclidean_domain.gcd_b x y)

theorem euclidean_domain.xgcd_aux_P {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) {r r' s t s' t' : R} :

P a b (r, s, t) → P a b (r', s', t') → P a b (euclidean_domain.xgcd_aux r s t r' s' t')

theorem euclidean_domain.gcd_eq_gcd_ab {R : Type u} [euclidean_domain R] [decidable_eq R] (a b : R) :

euclidean_domain.gcd a b = a * euclidean_domain.gcd_a a b + b * euclidean_domain.gcd_b a b

An explicit version of Bézout's lemma for Euclidean domains.

@[protected, instance]

def euclidean_domain.is_domain (R : Type u_1) [e : euclidean_domain R] :

def euclidean_domain.lcm {R : Type u} [euclidean_domain R] [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

euclidean_domain.lcm x y = x * y / euclidean_domain.gcd x y

theorem euclidean_domain.dvd_lcm_left {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :

x ∣ euclidean_domain.lcm x y

theorem euclidean_domain.dvd_lcm_right {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :

y ∣ euclidean_domain.lcm x y

theorem euclidean_domain.lcm_dvd {R : Type u} [euclidean_domain R] [decidable_eq R] {x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) :

euclidean_domain.lcm x y ∣ z

@[simp]

theorem euclidean_domain.lcm_dvd_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {x y z : R} :

euclidean_domain.lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z

@[simp]

theorem euclidean_domain.lcm_zero_left {R : Type u} [euclidean_domain R] [decidable_eq R] (x : R) :

euclidean_domain.lcm 0 x = 0

@[simp]

theorem euclidean_domain.lcm_zero_right {R : Type u} [euclidean_domain R] [decidable_eq R] (x : R) :

euclidean_domain.lcm x 0 = 0

@[simp]

theorem euclidean_domain.lcm_eq_zero_iff {R : Type u} [euclidean_domain R] [decidable_eq R] {x y : R} :

euclidean_domain.lcm x y = 0 ↔ x = 0 ∨ y = 0

@[simp]

theorem euclidean_domain.gcd_mul_lcm {R : Type u} [euclidean_domain R] [decidable_eq R] (x y : R) :

(euclidean_domain.gcd x y) * euclidean_domain.lcm x y = x * y

theorem euclidean_domain.mul_div_mul_cancel {R : Type u} [euclidean_domain R] {a b c : R} (ha : a ≠ 0) (hcb : c ∣ b) :

a * b / a * c = b / c

@[protected, instance]

def int.euclidean_domain :

euclidean_domain ℤ

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 := _, mul := has_mul.mul int.has_mul, mul_assoc := _, one := 1, 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}

@[protected, instance]

def field.to_euclidean_domain {K : Type u} [field K] :

euclidean_domain K

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 := _, mul := has_mul.mul (distrib.to_has_mul K), mul_assoc := _, one := 1, 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 := _}