Commit 2021-03-22 07:20 e7d74ba3

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.