Center_is_Intersection_of_Centralizers
Provedcenters-of-groupscentralizersproofwiki
The center of a group is the intersection of all the centralizers of its elements.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Center_is_Intersection_of_Centralizers {G : Type _} [Group G] :
Subgroup.center G = iInf (fun g : G => Subgroup.centralizer {g}) := by sorrySource