Inner_Automorphism_Group_Isomorphic_Quotient_Center_v2
Provedautomorphismcentergroup-theoryproofwikiquotient-group
The inner automorphism group Inn(G) is isomorphic to G/Z(G), where Z(G) is the center of G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Inner_Automorphism_Group_Isomorphic_Quotient_Center_v2 {G : Type _} [Group G] : Nonempty (G ⧸ Subgroup.center G ≃* (MonoidHom.range (MulAut.conj : G →* MulAut G))) := by sorrySource