English
Let G be a group acting on an additive monoid A by a distributive action. Then each g in G determines an additive automorphism of A by a ↦ g • a, and the assignment g ↦ (a ↦ g • a) is a monoid hom G →* AddAut(A).
Русский
Пусть группа G действует на аддитивном моноиде A распределенным образом. Тогда для каждого элемента g ∈ G отображение a ↦ g • a является аддитивным автоморфизмом A, и отображение g ↦ (a ↦ g • a) задаёт гомоморфизм моноидов G →* AddAut(A).
LaTeX
$$$\\text{toAddAut}: G \\to_* \\mathrm{AddAut}(A),\\quad (\\text{toAddAut}(g))(a) = g \\cdot a$$$
Lean4
/-- Each element of the group defines an additive monoid isomorphism.
This is a stronger version of `MulAction.toPerm`. -/
@[simps +simpRhs]
def toAddEquiv [DistribMulAction G A] (x : G) : A ≃+ A
where
__ := toAddMonoidHom A x
__ := MulAction.toPermHom G A x
