English
There is a pointwise action of α on Submonoid M given by S ↦ S.map (MulDistribMulAction.toMonoidEnd α M a); this defines a MulAction on Submonoid M.
Русский
Существует точечное действие α на Submonoid M, задаваемое S ↦ S.map (...); это образует MulAction на Submonoid M.
LaTeX
$$Submonoid.pointwiseMulAction : MulAction α (Submonoid M)$$
Lean4
/-- The action on a submonoid corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction α (Submonoid M)
where
smul a S := S.map (MulDistribMulAction.toMonoidEnd _ M a)
one_smul
S := by
change S.map _ = S
simpa only [map_one] using S.map_id
mul_smul _ _ S := (congr_arg (fun f : Monoid.End M => S.map f) (MonoidHom.map_mul _ _ _)).trans (S.map_map _ _).symm
