English
There is a natural action of a monoid M on AddSubgroup A by sending S to its image under the endomorphism induced by each a ∈ M.
Русский
Существует естественное действие моноида M на AddSubgroup A, переводя подпрацию S в образ под действием соответствующего концевого отображения.
LaTeX
$$$ a \cdot S = S.map(\\\\DistribMulAction.toAddMonoidEnd(M,A,a)) $$$
Lean4
/-- The action on an additive subgroup corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction M (AddSubgroup A)
where
smul a S := S.map (DistribMulAction.toAddMonoidEnd _ A a)
one_smul S := (congr_arg (fun f : AddMonoid.End A => S.map f) (MonoidHom.map_one _)).trans S.map_id
mul_smul _ _
S := (congr_arg (fun f : AddMonoid.End A => S.map f) (MonoidHom.map_mul _ _ _)).trans (S.map_map _ _).symm
