Commit 2021-03-15 09:03 1f47833e

feat(algebra/*, * : [regular, smul_with_zero, module/basic]): introduce mul_action_with_zero and M-regular elements (#6590) This PR has been split and there are now two separate PRs.

• #6590, this one, introducing smul_with_zero and mul_action_with_zero: two typeclasses to deal with multiplicative actions of monoid_with_zero, without the need to assume the presence of an addition!
• #6659, introducing M-regular elements, called smul_regular: the analogue of is_left_regular, but defined for an action of monoid_with_zero on a module M. This PR is a preparation for introducing M-regular elements. From the doc-string:

Introduce smul_with_zero

In analogy with the usual monoid action on a Type M, we introduce an action of a monoid_with_zero on a Type with 0. In particular, for Types R and M, both containing 0, we define smul_with_zero R M to be the typeclass where the products r • 0 and 0 • m vanish for all r ∈ R and all m ∈ M. Moreover, in the case in which R is a monoid_with_zero, we introduce the typeclass mul_action_with_zero R M, mimicking group actions and having an absorbing 0 in R. Thus, the action is required to be compatible with

• the unit of the monoid, acting as the identity;
• the zero of the monoid_with_zero, acting as zero;
• associativity of the monoid. Next, in a separate file, I introduce M-regular elements for a monoid_with_zero R with a mul_action_with_zero on a module M. The definition is simply to require that an element a : R is M-regular if the smultiplication M → M, given by m ↦ a • m is injective. We also prove some basic facts about M-regular elements. The PR further changes three further the files
• data/polynomial/coeffs;
• topology/algebra/module.lean;
• analysis/normed_space/bounded_linear_maps. The changes are prompted by a failure in CI. In each case, the change was tiny, mostly having to do with an exchange of a multiplication by a smultiplication or vice-versa.