Documentation

Mathlib.Algebra.EuclideanDomain.Defs

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 #

Main statements #

See Algebra.EuclideanDomain.Basic for most of the theorems about Eucliean domains, including Bézout's lemma.

See Algebra.EuclideanDomain.Instances for the facts 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≺ 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≺ 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 EuclideanDomain (R : Type u) extends CommRing , Nontrivial :
  • A division function (denoted /) on R. This satisfies the property b * (a / b) + a % b = a, where % denotes remainder.

    quotient : RRR
  • Division by zero should always give zero by convention.

    quotient_zero : ∀ (a : R), quotient a 0 = 0
  • A remainder function (denoted %) on R. This satisfies the property b * (a / b) + a % b = a, where / denotes quotient.

    remainder : RRR
  • The property that links the quotient and remainder functions. This allows us to compute GCDs and LCMs.

    quotient_mul_add_remainder_eq : ∀ (a b : R), b * quotient a b + remainder a b = a
  • A well-founded relation on R, satisfying r (a % b) b. This ensures that the GCD algorithm always terminates.

    r : RRProp
  • The relation r must be well-founded. This ensures that the GCD algorithm always terminates.

    r_wellFounded : WellFounded r
  • The relation r satisfies r (a % b) b.

    remainder_lt : (a : R) → {b : R} → b 0r (remainder a b) b
  • An additional constraint on r.

    mul_left_not_lt : ∀ (a : R) {b : R}, b 0¬r (a * b) a

A EuclideanDomain 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
    instance EuclideanDomain.instDiv {R : Type u} [inst : EuclideanDomain R] :
    Div R
    Equations
    • EuclideanDomain.instDiv = { div := EuclideanDomain.quotient }
    instance EuclideanDomain.instMod {R : Type u} [inst : EuclideanDomain R] :
    Mod R
    Equations
    • EuclideanDomain.instMod = { mod := EuclideanDomain.remainder }
    theorem EuclideanDomain.div_add_mod {R : Type u} [inst : EuclideanDomain R] (a : R) (b : R) :
    b * (a / b) + a % b = a
    theorem EuclideanDomain.mod_add_div {R : Type u} [inst : EuclideanDomain R] (a : R) (b : R) :
    a % b + b * (a / b) = a
    theorem EuclideanDomain.mod_add_div' {R : Type u} [inst : EuclideanDomain R] (m : R) (k : R) :
    m % k + m / k * k = m
    theorem EuclideanDomain.div_add_mod' {R : Type u} [inst : EuclideanDomain R] (m : R) (k : R) :
    m / k * k + m % k = m
    theorem EuclideanDomain.mod_eq_sub_mul_div {R : Type u_1} [inst : EuclideanDomain R] (a : R) (b : R) :
    a % b = a - b * (a / b)
    theorem EuclideanDomain.mod_lt {R : Type u} [inst : EuclideanDomain R] (a : R) {b : R} :
    b 0EuclideanDomain.r (a % b) b
    theorem EuclideanDomain.mul_right_not_lt {R : Type u} [inst : EuclideanDomain R] {a : R} (b : R) (h : a 0) :
    @[simp]
    theorem EuclideanDomain.mod_zero {R : Type u} [inst : EuclideanDomain R] (a : R) :
    a % 0 = a
    theorem EuclideanDomain.lt_one {R : Type u} [inst : EuclideanDomain R] (a : R) :
    EuclideanDomain.r a 1a = 0
    theorem EuclideanDomain.val_dvd_le {R : Type u} [inst : EuclideanDomain R] (a : R) (b : R) :
    b aa 0¬EuclideanDomain.r a b
    @[simp]
    theorem EuclideanDomain.div_zero {R : Type u} [inst : EuclideanDomain R] (a : R) :
    a / 0 = 0
    theorem EuclideanDomain.GCD.induction {R : Type u} [inst : EuclideanDomain R] {P : RRProp} (a : R) (b : R) (H0 : (x : R) → P 0 x) (H1 : (a b : R) → a 0P (b % a) aP a b) :
    P a b
    def EuclideanDomain.gcd {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] :
    RRR

    gcd a b is a (non-unique) element such that gcd a b ∣ a∣ a gcd a b ∣ b∣ b, and for any element c such that c ∣ a∣ a and c ∣ b∣ b, then c ∣ gcd a b∣ gcd a b

    Equations
    @[simp]
    theorem EuclideanDomain.gcd_zero_left {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] (a : R) :
    def EuclideanDomain.xgcdAux {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] :
    RRRRRRR × 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 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
    @[simp]
    theorem EuclideanDomain.xgcd_zero_left {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] {s : R} {t : R} {r' : R} {s' : R} {t' : R} :
    EuclideanDomain.xgcdAux 0 s t r' s' t' = (r', s', t')
    theorem EuclideanDomain.xgcdAux_rec {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] {r : R} {s : R} {t : R} {r' : R} {s' : R} {t' : R} (h : r 0) :
    EuclideanDomain.xgcdAux r s t r' s' t' = EuclideanDomain.xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
    def EuclideanDomain.xgcd {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] (x : R) (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 EuclideanDomain.gcdA {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] (x : R) (y : R) :
    R

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

    Equations
    def EuclideanDomain.gcdB {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] (x : R) (y : R) :
    R

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

    Equations
    @[simp]
    theorem EuclideanDomain.gcdA_zero_left {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] {s : R} :
    @[simp]
    theorem EuclideanDomain.gcdB_zero_left {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] {s : R} :
    def EuclideanDomain.lcm {R : Type u} [inst : EuclideanDomain R] [inst : DecidableEq R] (x : R) (y : R) :
    R

    lcm a b is a (non-unique) element such that a ∣ lcm a b∣ lcm a b b ∣ lcm a b∣ lcm a b, and for any element c such that a ∣ c∣ c and b ∣ c∣ c, then lcm a b ∣ c∣ c

    Equations