Normalizer_of_Center_is_Group
Provedcenternormalizersproofwiki
Let G be a group. Then the normalizer of the center Z(G) is G itself.
Preamble
import Mathlib.GroupTheory.Subgroup.Center
Formal statement
theorem Normalizer_of_Center_is_Group {G : Type _} [Group G] : (Subgroup.center G).normalizer = ⊤ := by sorrySource