English
There is a natural distributive action of AddAut(A) on A given by f • a = f(a); this action makes A a distributive module over AddAut(A).
Русский
Существует естественное распределенное действие группы аддитивных автоморфизмов AddAut(A) на A, заданное f • a = f(a); это действие делает A модулем над AddAut(A) в дискретном смысле.
LaTeX
$$$\\text{applyDistribMulAction} : \\mathrm{AddAut}(A) \\curvearrowright A \\\\smul := (\\cdot \\,|\\, \\cdot),\\; 1 \\smul a = a,\\; (fg) \\smul a = f(g(a))$$
Lean4
/-- The tautological action by `AddAut A` on `A`.
This generalizes `Function.End.applyMulAction`. -/
instance applyDistribMulAction [AddMonoid A] : DistribMulAction (AddAut A) A
where
smul := (· <| ·)
smul_zero := map_zero
smul_add := map_add
one_smul _ := rfl
mul_smul _ _ _ := rfl
