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

source
theorem IsLeftRegular.right_of_commute {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) (h : IsLeftRegular a) :
IsRightRegular a
source
theorem IsAddLeftRegular.right_of_addCommute {R : Type u_1} [Add R] {a : R} (ca : ∀ (b : R), AddCommute a b) (h : IsAddLeftRegular a) :
IsAddRightRegular a
source
theorem IsRightRegular.left_of_commute {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) (h : IsRightRegular a) :
IsLeftRegular a
source
theorem IsAddRightRegular.left_of_addCommute {R : Type u_1} [Add R] {a : R} (ca : ∀ (b : R), AddCommute a b) (h : IsAddRightRegular a) :
IsAddLeftRegular a
source
theorem Commute.isRightRegular_iff {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) :
IsRightRegular a ↔ IsLeftRegular a
source
theorem AddCommute.isAddRightRegular_iff {R : Type u_1} [Add R] {a : R} (ca : ∀ (b : R), AddCommute a b) :
IsAddRightRegular a ↔ IsAddLeftRegular a
source
theorem Commute.isRegular_iff {R : Type u_1} [Mul R] {a : R} (ca : ∀ (b : R), Commute a b) :
IsRegular a ↔ IsLeftRegular a
source
theorem AddCommute.isAddRegular_iff {R : Type u_1} [Add R] {a : R} (ca : ∀ (b : R), AddCommute a b) :
IsAddRegular a ↔ IsAddLeftRegular a
source
theorem IsLeftRegular.mul {R : Type u_1} [Semigroup R] {a b : R} (lra : IsLeftRegular a) (lrb : IsLeftRegular b) :
IsLeftRegular (a * b)

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

source
theorem IsAddLeftRegular.add {R : Type u_1} [AddSemigroup R] {a b : R} (lra : IsAddLeftRegular a) (lrb : IsAddLeftRegular b) :
IsAddLeftRegular (a + b)

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

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

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

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

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

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

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

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

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

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

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

source
theorem IsAddLeftRegular.of_add {R : Type u_1} [AddSemigroup R] {a b : R} (ab : IsAddLeftRegular (a + b)) :
IsAddLeftRegular 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.

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

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

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

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.

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

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

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

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.

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

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

source
@[simp]
theorem add_isAddRightRegular_iff {R : Type u_1} [AddSemigroup R] {a : R} (b : R) (ha : IsAddRightRegular a) :
IsAddRightRegular (b + a) ↔ IsAddRightRegular b

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.

source
theorem isRegular_mul_and_mul_iff {R : Type u_1} [Semigroup R] {a b : R} :
IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

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

source
theorem isAddRegular_add_and_add_iff {R : Type u_1} [AddSemigroup R] {a b : R} :
IsAddRegular (a + b) ∧ IsAddRegular (b + a) ↔ IsAddRegular a ∧ IsAddRegular b

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

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

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

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

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

source
theorem isRegular_one {R : Type u_1} [MulOneClass R] :
IsRegular 1

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

source
theorem isAddRegular_zero {R : Type u_1} [AddZeroClass R] :
IsAddRegular 0

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

source
theorem isRegular_mul_iff {R : Type u_1} [CommSemigroup R] {a b : R} :
IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b

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

source
theorem isAddRegular_add_iff {R : Type u_1} [AddCommSemigroup R] {a b : R} :
IsAddRegular (a + b) ↔ IsAddRegular a ∧ IsAddRegular b

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

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

An element admitting a left inverse is left-regular.

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

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

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

An element admitting a right inverse is right-regular.

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

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

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

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

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

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

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

A unit in a monoid is regular.

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

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

source
theorem IsLeftRegular.pow {R : Type u_1} [Monoid R] {a : R} (n : ℕ) (rla : IsLeftRegular a) :
IsLeftRegular (a ^ n)

Any power of a left-regular element is left-regular.

source
theorem IsAddLeftRegular.nsmul {R : Type u_1} [AddMonoid R] {a : R} (n : ℕ) (rla : IsAddLeftRegular a) :
IsAddLeftRegular (n • a)
source
theorem IsRightRegular.pow {R : Type u_1} [Monoid R] {a : R} (n : ℕ) (rra : IsRightRegular a) :
IsRightRegular (a ^ n)

Any power of a right-regular element is right-regular.

source
theorem IsAddRightRegular.nsmul {R : Type u_1} [AddMonoid R] {a : R} (n : ℕ) (rra : IsAddRightRegular a) :
IsAddRightRegular (n • a)
source
theorem IsRegular.pow {R : Type u_1} [Monoid R] {a : R} (n : ℕ) (ra : IsRegular a) :
IsRegular (a ^ n)

Any power of a regular element is regular.

source
theorem IsAddRegular.nsmul {R : Type u_1} [AddMonoid R] {a : R} (n : ℕ) (ra : IsAddRegular a) :
IsAddRegular (n • a)
source
theorem IsLeftRegular.pow_iff {R : Type u_1} [Monoid R] {a : R} {n : ℕ} (n0 : 0 < n) :
IsLeftRegular (a ^ n) ↔ IsLeftRegular a

An element `a` is left-regular if and only if a positive power of `a` is left-regular.

source
theorem IsAddLeftRegular.nsmul_iff {R : Type u_1} [AddMonoid R] {a : R} {n : ℕ} (n0 : 0 < n) :
IsAddLeftRegular (n • a) ↔ IsAddLeftRegular a
source
theorem IsRightRegular.pow_iff {R : Type u_1} [Monoid R] {a : R} {n : ℕ} (n0 : 0 < n) :
IsRightRegular (a ^ n) ↔ IsRightRegular a

An element `a` is right-regular if and only if a positive power of `a` is right-regular.

source
theorem IsAddRightRegular.nsmul_iff {R : Type u_1} [AddMonoid R] {a : R} {n : ℕ} (n0 : 0 < n) :
IsAddRightRegular (n • a) ↔ IsAddRightRegular a
source
theorem IsRegular.pow_iff {R : Type u_1} [Monoid R] {a : R} {n : ℕ} (n0 : 0 < n) :
IsRegular (a ^ n) ↔ IsRegular a

An element `a` is regular if and only if a positive power of `a` is regular.

source
theorem IsAddRegular.nsmul_iff {R : Type u_1} [AddMonoid R] {a : R} {n : ℕ} (n0 : 0 < n) :
IsAddRegular (n • a) ↔ IsAddRegular a
source
@[simp]
theorem IsLeftRegular.mul_left_eq_self_iff {R : Type u_1} [Monoid R] {a b : R} (ha : IsLeftRegular a) :
a * b = a ↔ b = 1
source
@[simp]
theorem IsAddLeftRegular.add_left_eq_self_iff {R : Type u_1} [AddMonoid R] {a b : R} (ha : IsAddLeftRegular a) :
a + b = a ↔ b = 0
source
@[simp]
theorem IsRightRegular.mul_right_eq_self_iff {R : Type u_1} [Monoid R] {a b : R} (ha : IsRightRegular a) :
b * a = a ↔ b = 1
source
@[simp]
theorem IsAddRightRegular.add_right_eq_self_iff {R : Type u_1} [AddMonoid R] {a b : R} (ha : IsAddRightRegular a) :
b + a = a ↔ b = 0