English
There is a strengthened action of α on Submodule R M compatible with zero, extending the pointwise distributive action.
Русский
Существуют усиленное действие α на Submodule R M, совместимое с нулём, продолжающее точечно-дистрибутивное действие.
LaTeX
$$$\\text{MulActionWithZero } α (Submodule\\, R\\, M)$$$
Lean4
/-- The action on a submodule corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale.
This is a stronger version of `Submodule.pointwiseDistribMulAction`. Note that `add_smul` does
not hold so this cannot be stated as a `Module`. -/
protected def pointwiseMulActionWithZero : MulActionWithZero α (Submodule R M) :=
{ Submodule.pointwiseDistribMulAction with
zero_smul := fun S => (congr_arg (fun f : M →ₗ[R] M => S.map f) (LinearMap.ext <| zero_smul α)).trans S.map_zero }
