Regular elements #
We introduce left-regular, right-regular and regular elements.
By definition, a regular element in a commutative ring is a non-zero divisor.
Lemma 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 0
.
The final goal is to develop part of the API to prove, eventually, results about non-zero-divisors.
A left-regular element is an element c
such that multiplication on the left by c
is injective on the left.
Equations
A right-regular element is an element c
such that multiplication on the right by c
is injective on the right.
Equations
- is_right_regular c = function.injective (λ (_x : R), _x * c)
- left : is_left_regular c
- right : is_right_regular c
A regular element is an element c
such that multiplication by c
both on the left and
on the right is injective.
In a semigroup, the product of left-regular elements is left-regular.
In a semigroup, the product of right-regular elements is right-regular.
If an element b
becomes left-regular after multiplying it on the left by a left-regular
element, then b
is left-regular.
An element is left-regular if and only if multiplying it on the left by a left-regular element is left-regular.
If an element b
becomes right-regular after multiplying it on the right by a right-regular
element, then b
is right-regular.
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 regular if and only if both products a * b
and b * a
are regular.
The "most used" implication of mul_and_mul_iff
, with split hypotheses, instead of ∧
.
Any power of a left-regular element is left-regular.
Any power of a right-regular element is right-regular.
Any power of a regular element is regular.
An element a
is left-regular if and only if a positive power of a
is left-regular.
An element a
is right-regular if and only if a positive power of a
is right-regular.
An element a
is regular if and only if a positive power of a
is regular.
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 mul_zero_class
, the 0
element is not left-regular.
The element 0
is right-regular if and only if R
is trivial.
In a non-trivial mul_zero_class
, the 0
element is not right-regular.
The element 0
is regular if and only if R
is trivial.
A left-regular element of a nontrivial
mul_zero_class
is non-zero.
A right-regular element of a nontrivial
mul_zero_class
is non-zero.
A regular element of a nontrivial
mul_zero_class
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.
A product is regular if and only if the factors are.
An element admitting a left inverse is left-regular.
An element admitting a right inverse is right-regular.
If R
is a monoid, an element in units R
is regular.
A unit in a monoid is regular.
Elements of a left cancel semigroup are left regular.
Elements of a right cancel semigroup are right regular.
Elements of a cancel monoid are regular. Cancel semigroups do not appear to exist.
Non-zero elements of an integral domain are regular.
In a non-trivial integral domain, an element is regular iff it is non-zero.