English
There is a natural equivalence between AddAut (Additive G) and MulAut G for any additive group G; i.e., their automorphism groups are canonically isomorphic.
Русский
Существует естественная эквивалентность между AddAut (Additive G) и MulAut G для любой аддитивной группы G; то есть их группы автоморфизмов канонически изоморфны.
LaTeX
$$$\mathrm{AddAutAdditive} : \mathrm{AddAut}(\mathrm{Additive} G) \simeq_* \mathrm{MulAut} G$$$
Lean4
/-- `Additive G` and `G` have isomorphic automorphism groups. -/
@[simps!]
def AddAutAdditive [Group G] : AddAut (Additive G) ≃* MulAut G :=
{ MulEquiv.toAdditive.symm with map_mul' := fun _ _ ↦ rfl }
