Inner_Automorphisms_form_Normal_Subgroup_of_Automorphism_Group
Provedautomorphismsnormal-subgroupsproofwiki
The set of inner automorphisms of G forms a normal subgroup of Aut(G).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Inner_Automorphisms_form_Normal_Subgroup_of_Automorphism_Group {G : Type _} [Group G] (a g : G) : a * g * a⁻¹ = (MulAut.conj a) g := by sorrySource