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

Tags #

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

class EuclideanDomain (R : Type u) extends CommRing , Nontrivial :

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 : RRR
  • add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
  • zero : R
  • zero_add : ∀ (a : R), 0 + a = a
  • add_zero : ∀ (a : R), a + 0 = a
  • nsmul : RR
  • nsmul_zero : ∀ (x : R), AddMonoid.nsmul 0 x = 0
  • nsmul_succ : ∀ (n : ) (x : R), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
  • add_comm : ∀ (a b : R), a + b = b + a
  • mul : RRR
  • left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
  • right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
  • zero_mul : ∀ (a : R), 0 * a = 0
  • mul_zero : ∀ (a : R), a * 0 = 0
  • mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
  • one : R
  • one_mul : ∀ (a : R), 1 * a = a
  • mul_one : ∀ (a : R), a * 1 = a
  • natCast : R
  • natCast_zero : NatCast.natCast 0 = 0
  • natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
  • npow : RR
  • 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 : RR
  • sub : RRR
  • sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
  • zsmul : RR
  • 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
  • neg_add_cancel : ∀ (a : R), -a + a = 0
  • intCast : R
  • intCast_ofNat : ∀ (n : ), IntCast.intCast n = n
  • intCast_negSucc : ∀ (n : ), IntCast.intCast (Int.negSucc n) = -(n + 1)
  • mul_comm : ∀ (a b : R), a * b = b * a
  • exists_pair_ne : ∃ (x : R), ∃ (y : R), x y
  • quotient : RRR

    A division function (denoted /) on R. This satisfies the property b * (a / b) + a % b = a, where % denotes remainder.

  • quotient_zero : ∀ (a : R), EuclideanDomain.quotient a 0 = 0

    Division by zero should always give zero by convention.

  • remainder : RRR

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

  • 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 : RRProp

    A well-founded relation on R, satisfying r (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 0EuclideanDomain.r (EuclideanDomain.remainder a b) b

    The relation r satisfies r (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.

    theorem EuclideanDomain.r_wellFounded {R : Type u} [self : EuclideanDomain R] :
    WellFounded EuclideanDomain.r

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

    theorem EuclideanDomain.remainder_lt {R : Type u} [self : EuclideanDomain R] (a : R) {b : R} :

    The relation r satisfies r (a % b) b.

    theorem EuclideanDomain.mul_left_not_lt {R : Type u} [self : EuclideanDomain R] (a : R) {b : R} :
    b 0¬EuclideanDomain.r (a * b) a

    An additional constraint on r.

    Equations
    • EuclideanDomain.wellFoundedRelation = { rel := EuclideanDomain.r, wf := }
    Instances For
      instance EuclideanDomain.isWellFounded {R : Type u} [EuclideanDomain R] :
      IsWellFounded R fun (x1 x2 : R) => EuclideanDomain.r x1 x2
      Equations
      • =
      @[instance 70]
      Equations
      • EuclideanDomain.instDiv = { div := EuclideanDomain.quotient }
      @[instance 70]
      Equations
      • EuclideanDomain.instMod = { mod := EuclideanDomain.remainder }
      theorem EuclideanDomain.div_add_mod {R : Type u} [EuclideanDomain R] (a : R) (b : R) :
      b * (a / b) + a % b = a
      theorem EuclideanDomain.mod_add_div {R : Type u} [EuclideanDomain R] (a : R) (b : R) :
      a % b + b * (a / b) = a
      theorem EuclideanDomain.mod_add_div' {R : Type u} [EuclideanDomain R] (m : R) (k : R) :
      m % k + m / k * k = m
      theorem EuclideanDomain.div_add_mod' {R : Type u} [EuclideanDomain R] (m : R) (k : R) :
      m / k * k + m % k = m
      theorem EuclideanDomain.mod_eq_sub_mul_div {R : Type u_1} [EuclideanDomain R] (a : R) (b : R) :
      a % b = a - b * (a / b)
      theorem EuclideanDomain.mod_lt {R : Type u} [EuclideanDomain R] (a : R) {b : R} :
      b 0EuclideanDomain.r (a % b) b
      theorem EuclideanDomain.mul_right_not_lt {R : Type u} [EuclideanDomain R] {a : R} (b : R) (h : a 0) :
      @[simp]
      theorem EuclideanDomain.mod_zero {R : Type u} [EuclideanDomain R] (a : R) :
      a % 0 = a
      theorem EuclideanDomain.lt_one {R : Type u} [EuclideanDomain R] (a : R) :
      EuclideanDomain.r a 1a = 0
      theorem EuclideanDomain.val_dvd_le {R : Type u} [EuclideanDomain R] (a : R) (b : R) :
      b aa 0¬EuclideanDomain.r a b
      @[simp]
      theorem EuclideanDomain.div_zero {R : Type u} [EuclideanDomain R] (a : R) :
      a / 0 = 0
      @[irreducible]
      theorem EuclideanDomain.GCD.induction {R : Type u} [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
      @[irreducible]
      def EuclideanDomain.gcd {R : Type u} [EuclideanDomain R] [DecidableEq R] (a : R) (b : 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
      Instances For
        @[irreducible]
        def EuclideanDomain.xgcdAux {R : Type u} [EuclideanDomain R] [DecidableEq R] (r : R) (s : R) (t : R) (r' : R) (s' : R) (t' : 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 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
        Instances For
          @[simp]
          theorem EuclideanDomain.xgcd_zero_left {R : Type u} [EuclideanDomain R] [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} [EuclideanDomain R] [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} [EuclideanDomain R] [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
          Instances For
            def EuclideanDomain.gcdA {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (y : R) :
            R

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

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

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

              Equations
              Instances For
                def EuclideanDomain.lcm {R : Type u} [EuclideanDomain R] [DecidableEq R] (x : R) (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
                Instances For