Documentation

Mathlib.Algebra.Regular.Basic

Regular elements #

We introduce left-regular, right-regular and regular elements, along with their to_additive analogues add-left-regular, add-right-regular and add-regular elements.

By definition, a regular element in a commutative ring is a non-zero divisor. Lemma isRegular_of_ne_zero implies that every non-zero element of an integral domain is regular. Since it assumes that the ring is a CancelMonoidWithZero it applies also, for instance, to .

The lemmas in Section MulZeroClass show that the 0 element is (left/right-)regular if and only if the MulZeroClass is trivial. This is useful when figuring out stopping conditions for regular sequences: if 0 is ever an element of a regular sequence, then we can extend the sequence by adding one further 0.

The final goal is to develop part of the API to prove, eventually, results about non-zero-divisors.

def IsAddLeftRegular {R : Type u_1} [Add R] (c : R) :

An add-left-regular element is an element c such that addition on the left by c is injective.

Equations
Instances For
    def IsLeftRegular {R : Type u_1} [Mul R] (c : R) :

    A left-regular element is an element c such that multiplication on the left by c is injective.

    Equations
    Instances For
      def IsAddRightRegular {R : Type u_1} [Add R] (c : R) :

      An add-right-regular element is an element c such that addition on the right by c is injective.

      Equations
      Instances For
        def IsRightRegular {R : Type u_1} [Mul R] (c : R) :

        A right-regular element is an element c such that multiplication on the right by c is injective.

        Equations
        Instances For
          structure IsAddRegular {R : Type u_2} [Add R] (c : R) :

          An add-regular element is an element c such that addition by c both on the left and on the right is injective.

          Instances For
            theorem IsAddRegular.left {R : Type u_2} [Add R] {c : R} (self : IsAddRegular c) :

            An add-regular element c is left-regular

            theorem IsAddRegular.right {R : Type u_2} [Add R] {c : R} (self : IsAddRegular c) :

            An add-regular element c is right-regular

            structure IsRegular {R : Type u_1} [Mul R] (c : R) :

            A regular element is an element c such that multiplication by c both on the left and on the right is injective.

            Instances For
              @[simp]
              theorem IsRegular.left {R : Type u_1} [Mul R] {c : R} (self : IsRegular c) :

              A regular element c is left-regular

              @[simp]
              theorem IsRegular.right {R : Type u_1} [Mul R] {c : R} (self : IsRegular c) :

              A regular element c is right-regular

              abbrev isAddRegular_iff.match_2 {R : Type u_1} [Add R] {c : R} (motive : IsAddLeftRegular c IsAddRightRegular cProp) :
              ∀ (x : IsAddLeftRegular c IsAddRightRegular c), (∀ (h1 : IsAddLeftRegular c) (h2 : IsAddRightRegular c), motive )motive x
              Equations
              • =
              Instances For
                abbrev isAddRegular_iff.match_1 {R : Type u_1} [Add R] {c : R} (motive : IsAddRegular cProp) :
                ∀ (x : IsAddRegular c), (∀ (h1 : IsAddLeftRegular c) (h2 : IsAddRightRegular c), motive )motive x
                Equations
                • =
                Instances For
                  theorem IsLeftRegular.right_of_commute {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) (h : IsLeftRegular a) :
                  theorem IsRightRegular.left_of_commute {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) (h : IsRightRegular a) :
                  theorem Commute.isRightRegular_iff {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) :
                  theorem Commute.isRegular_iff {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) :
                  theorem IsAddLeftRegular.add {R : Type u_1} [AddSemigroup R] {a : R} {b : R} (lra : IsAddLeftRegular a) (lrb : IsAddLeftRegular b) :

                  In an additive semigroup, the sum of add-left-regular elements is add-left.regular.

                  theorem IsLeftRegular.mul {R : Type u_1} [Semigroup R] {a : R} {b : R} (lra : IsLeftRegular a) (lrb : IsLeftRegular b) :

                  In a semigroup, the product of left-regular elements is left-regular.

                  theorem IsAddRightRegular.add {R : Type u_1} [AddSemigroup R] {a : R} {b : R} (rra : IsAddRightRegular a) (rrb : IsAddRightRegular b) :

                  In an additive semigroup, the sum of add-right-regular elements is add-right-regular.

                  theorem IsRightRegular.mul {R : Type u_1} [Semigroup R] {a : R} {b : R} (rra : IsRightRegular a) (rrb : IsRightRegular b) :

                  In a semigroup, the product of right-regular elements is right-regular.

                  theorem IsAddRegular.add {R : Type u_1} [AddSemigroup R] {a : R} {b : R} (rra : IsAddRegular a) (rrb : IsAddRegular b) :

                  In an additive semigroup, the sum of add-regular elements is add-regular.

                  theorem IsRegular.mul {R : Type u_1} [Semigroup R] {a : R} {b : R} (rra : IsRegular a) (rrb : IsRegular b) :
                  IsRegular (a * b)

                  In a semigroup, the product of regular elements is regular.

                  theorem IsAddLeftRegular.of_add {R : Type u_1} [AddSemigroup R] {a : R} {b : R} (ab : IsAddLeftRegular (a + b)) :

                  If an element b becomes add-left-regular after adding to it on the left an add-left-regular element, then b is add-left-regular.

                  theorem IsLeftRegular.of_mul {R : Type u_1} [Semigroup R] {a : R} {b : R} (ab : IsLeftRegular (a * b)) :

                  If an element b becomes left-regular after multiplying it on the left by a left-regular element, then b is left-regular.

                  @[simp]
                  theorem add_isAddLeftRegular_iff {R : Type u_1} [AddSemigroup R] {a : R} (b : R) (ha : IsAddLeftRegular a) :

                  An element is add-left-regular if and only if adding to it on the left an add-left-regular element is add-left-regular.

                  @[simp]
                  theorem mul_isLeftRegular_iff {R : Type u_1} [Semigroup R] {a : R} (b : R) (ha : IsLeftRegular a) :

                  An element is left-regular if and only if multiplying it on the left by a left-regular element is left-regular.

                  theorem IsAddRightRegular.of_add {R : Type u_1} [AddSemigroup R] {a : R} {b : R} (ab : IsAddRightRegular (b + a)) :

                  If an element b becomes add-right-regular after adding to it on the right an add-right-regular element, then b is add-right-regular.

                  theorem IsRightRegular.of_mul {R : Type u_1} [Semigroup R] {a : R} {b : R} (ab : IsRightRegular (b * a)) :

                  If an element b becomes right-regular after multiplying it on the right by a right-regular element, then b is right-regular.

                  @[simp]

                  An element is add-right-regular if and only if adding it on the right to an add-right-regular element is add-right-regular.

                  @[simp]
                  theorem mul_isRightRegular_iff {R : Type u_1} [Semigroup R] {a : R} (b : R) (ha : IsRightRegular a) :

                  An element is right-regular if and only if multiplying it on the right with a right-regular element is right-regular.

                  Two elements a and b are add-regular if and only if both sums a + b and b + a are add-regular.

                  theorem isRegular_mul_and_mul_iff {R : Type u_1} [Semigroup R] {a : R} {b : R} :

                  Two elements a and b are regular if and only if both products a * b and b * a are regular.

                  theorem IsAddRegular.and_of_add_of_add {R : Type u_1} [AddSemigroup R] {a : R} {b : R} (ab : IsAddRegular (a + b)) (ba : IsAddRegular (b + a)) :

                  The "most used" implication of add_and_add_iff, with split hypotheses, instead of .

                  theorem IsRegular.and_of_mul_of_mul {R : Type u_1} [Semigroup R] {a : R} {b : R} (ab : IsRegular (a * b)) (ba : IsRegular (b * a)) :

                  The "most used" implication of mul_and_mul_iff, with split hypotheses, instead of .

                  The element 0 is left-regular if and only if R is trivial.

                  The element 0 is right-regular if and only if R is trivial.

                  The element 0 is regular if and only if R is trivial.

                  The element 0 is left-regular if and only if R is trivial.

                  In a non-trivial MulZeroClass, the 0 element is not left-regular.

                  The element 0 is right-regular if and only if R is trivial.

                  In a non-trivial MulZeroClass, the 0 element is not right-regular.

                  The element 0 is regular if and only if R is trivial.

                  theorem IsLeftRegular.ne_zero {R : Type u_1} [MulZeroClass R] {a : R} [Nontrivial R] (la : IsLeftRegular a) :
                  a 0

                  A left-regular element of a Nontrivial MulZeroClass is non-zero.

                  theorem IsRightRegular.ne_zero {R : Type u_1} [MulZeroClass R] {a : R} [Nontrivial R] (ra : IsRightRegular a) :
                  a 0

                  A right-regular element of a Nontrivial MulZeroClass is non-zero.

                  theorem IsRegular.ne_zero {R : Type u_1} [MulZeroClass R] {a : R} [Nontrivial R] (la : IsRegular a) :
                  a 0

                  A regular element of a Nontrivial MulZeroClass is non-zero.

                  In a non-trivial ring, the element 0 is not left-regular -- with typeclasses.

                  In a non-trivial ring, the element 0 is not right-regular -- with typeclasses.

                  In a non-trivial ring, the element 0 is not regular -- with typeclasses.

                  @[simp]
                  theorem IsLeftRegular.mul_left_eq_zero_iff {R : Type u_1} [MulZeroClass R] {a : R} {b : R} (hb : IsLeftRegular b) :
                  b * a = 0 a = 0
                  @[simp]
                  theorem IsRightRegular.mul_right_eq_zero_iff {R : Type u_1} [MulZeroClass R] {a : R} {b : R} (hb : IsRightRegular b) :
                  a * b = 0 a = 0

                  If adding 0 on either side is the identity, 0 is regular.

                  theorem isRegular_one {R : Type u_1} [MulOneClass R] :

                  If multiplying by 1 on either side is the identity, 1 is regular.

                  theorem isAddRegular_add_iff {R : Type u_1} [AddCommSemigroup R] {a : R} {b : R} :

                  A sum is add-regular if and only if the summands are.

                  theorem isRegular_mul_iff {R : Type u_1} [CommSemigroup R] {a : R} {b : R} :

                  A product is regular if and only if the factors are.

                  theorem isAddLeftRegular_of_add_eq_zero {R : Type u_1} [AddMonoid R] {a : R} {b : R} (h : b + a = 0) :

                  An element admitting a left additive opposite is add-left-regular.

                  theorem isLeftRegular_of_mul_eq_one {R : Type u_1} [Monoid R] {a : R} {b : R} (h : b * a = 1) :

                  An element admitting a left inverse is left-regular.

                  theorem isAddRightRegular_of_add_eq_zero {R : Type u_1} [AddMonoid R] {a : R} {b : R} (h : a + b = 0) :

                  An element admitting a right additive opposite is add-right-regular.

                  theorem isRightRegular_of_mul_eq_one {R : Type u_1} [Monoid R] {a : R} {b : R} (h : a * b = 1) :

                  An element admitting a right inverse is right-regular.

                  theorem AddUnits.isAddRegular {R : Type u_1} [AddMonoid R] (a : AddUnits R) :

                  If R is an additive monoid, an element in add_units R is add-regular.

                  theorem Units.isRegular {R : Type u_1} [Monoid R] (a : Rˣ) :

                  If R is a monoid, an element in is regular.

                  theorem IsAddUnit.isAddRegular {R : Type u_1} [AddMonoid R] {a : R} (ua : IsAddUnit a) :

                  An additive unit in an additive monoid is add-regular.

                  theorem IsUnit.isRegular {R : Type u_1} [Monoid R] {a : R} (ua : IsUnit a) :

                  A unit in a monoid is regular.

                  theorem IsAddLeftRegular.all {R : Type u_1} [Add R] [IsLeftCancelAdd R] (g : R) :

                  If all additions cancel on the left then every element is add-left-regular.

                  theorem IsLeftRegular.all {R : Type u_1} [Mul R] [IsLeftCancelMul R] (g : R) :

                  If all multiplications cancel on the left then every element is left-regular.

                  theorem IsAddRightRegular.all {R : Type u_1} [Add R] [IsRightCancelAdd R] (g : R) :

                  If all additions cancel on the right then every element is add-right-regular.

                  theorem IsRightRegular.all {R : Type u_1} [Mul R] [IsRightCancelMul R] (g : R) :

                  If all multiplications cancel on the right then every element is right-regular.

                  theorem IsAddRegular.all {R : Type u_1} [Add R] [IsCancelAdd R] (g : R) :

                  If all additions cancel then every element is add-regular.

                  theorem IsRegular.all {R : Type u_1} [Mul R] [IsCancelMul R] (g : R) :

                  If all multiplications cancel then every element is regular.

                  theorem isRegular_of_ne_zero {R : Type u_1} [MulZeroClass R] [IsCancelMulZero R] {a : R} (a0 : a 0) :

                  Non-zero elements of an integral domain are regular.

                  theorem isRegular_iff_ne_zero {R : Type u_1} [MulZeroClass R] [IsCancelMulZero R] {a : R} [Nontrivial R] :

                  In a non-trivial integral domain, an element is regular iff it is non-zero.