mathlib

1f47833e - feat(algebra/*, * : [regular, smul_with_zero, module/basic]): introduce `mul_action_with_zero` and `M`-regular elements (#6590)

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. Co-authored-by: Vierkantor <vierkantor@vierkantor.com> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>