feat(algebra/smul_regular): add `M`-regular elements (#6659)
This PR extends PR #6590, that is now merged. The current PR contains the actual API to work with `M`-regular elements `r : R`, called `is_smul_regular M r`.
Zulip:
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews
From the doc-string:
### Action of regular elements on a module
We introduce `M`-regular elements, in the context of an `R`-module `M`. The corresponding
predicate is called `is_smul_regular`.
There are very limited typeclass assumptions on `R` and `M`, but the "mathematical" case of interest
is a commutative ring `R` acting an a module `M`. Since the properties are "multiplicative", there
is no actual requirement of having an addition, but there is a zero in both `R` and `M`.
Smultiplications involving `0` are, of course, all trivial.
The defining property is that an element `a ∈ R` is `M`-regular if the smultiplication map
`M → M`, defined by `m ↦ a • m`, is injective.
This property is the direct generalization to modules of the property `is_left_regular` defined in
`algebra/regular`. Lemma `is_smul_regular.is_left_regular_iff` shows that indeed the two notions
coincide.
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
