Regular elements #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We introduce left-regular, right-regular and regular elements, along with their
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.
is_regular_of_ne_zero implies that every non-zero element of an integral domain is regular.
Since it assumes that the ring is a
cancel_monoid_with_zero it applies also, for instance, to
The lemmas in Section
mul_zero_class show that the
0 element is (left/right-)regular if and
only if the
mul_zero_class 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
The final goal is to develop part of the API to prove, eventually, results about non-zero-divisors.
An element is add-right-regular if and only if adding it on the right to a add-right-regular element is add-right-regular.
Elements of an add right cancel semigroup are add-right-regular