English
The action described above defines a monoid homomorphism from G into the group of additive automorphisms of A, given by g ↦ (a ↦ g • a).
Русский
Описанное выше действие порождает гомоморфизм моноидов из G в группу аддитивных автоморфизмов A, отображение g ↦ (a ↦ g • a).
LaTeX
$$$\\text{toAddAut} : G \\to_* \\mathrm{AddAut}(A),\\quad (\\text{toAddAut}(g))(a) = g \\cdot a, \\; g,h\\in G,\\; \\text{toAddAut}(gh) = \\text{toAddAut}(g) \\circ \\text{toAddAut}(h)$$$
Lean4
/-- Each element of the group defines an additive monoid isomorphism.
This is a stronger version of `MulAction.toPermHom`. -/
@[simps]
def toAddAut [DistribMulAction G A] : G →* AddAut A
where
toFun := toAddEquiv _
map_one' := AddEquiv.ext (one_smul _)
map_mul' _ _ := AddEquiv.ext (mul_smul _ _)
