Kernel_of_Inner_Automorphism_Group_is_Center

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

automorphismscenterkernelsproofwiki

Let κ: G → Inn(G) be the map from a group to its inner automorphism group. Then ker(κ) = Z(G), the center of G.

Preamble

import Mathlib.GroupTheory.GroupAction.ConjAct
import Mathlib.GroupTheory.Subgroup.Center

Formal statement

theorem Kernel_of_Inner_Automorphism_Group_is_Center {G : Type _} [Group G] : (MulAut.conj : G →* MulAut G).ker = Subgroup.center G := by sorry

Source