MulAutMultiplicative — Mathlib

English

There is an isomorphism between the automorphism group of the multiplicative view of G and the additive automorphism group of G when G is abelian.

Русский

Существует изоморфизм между группой автоморфизмов MulAut (Multiplicative G) и AddAut G при условии, что G является аддитивной группой.

LaTeX

$$$\mathrm{MulAut}(\mathrm{Multiplicative} G) \cong \mathrm{AddAut} G$$$

Lean4

/-- `Multiplicative G` and `G` have isomorphic automorphism groups. -/
@[simps!]
def MulAutMultiplicative [AddGroup G] : MulAut (Multiplicative G) ≃* AddAut G :=
  { AddEquiv.toMultiplicative.symm with map_mul' := fun _ _ ↦ rfl }

Похожие утверждения