Conjugacy_Class_of_Element_of_Center_is_Singleton
Provedcenterconjugacy-classgroup-theoryproofwiki
An element of a group is in the center if and only if its conjugacy class is a singleton.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Conjugacy_Class_of_Element_of_Center_is_Singleton {G : Type _} [Group G] (g : G) : g ∈ Subgroup.center G ↔ ∀ a : G, a * g * a⁻¹ = g := by sorrySource