English
There is a natural M-action on Subsemiring R defined by smul a S = map φ_a S.
Русский
Существует естественное действие множества M на Subsemiring R, задаваемое smul a S = map φ_a S.
LaTeX
$$$\\text{pointwiseMulAction} : M \\curvearrowright \\text{Subsemiring}(R)$ with $a \\cdot S = S.map(\\text{MulSemiringAction.toRingHom}(M,R,a))$$$
Lean4
/-- The action on a subsemiring corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseMulAction : MulAction M (Subsemiring R)
where
smul a S := S.map (MulSemiringAction.toRingHom _ _ a)
one_smul S := (congr_arg (fun f => S.map f) (RingHom.ext <| one_smul M)).trans S.map_id
mul_smul _a₁ _a₂ S := (congr_arg (fun f => S.map f) (RingHom.ext <| mul_smul _ _)).trans (S.map_map _ _).symm
