Center_of_Group_is_Normal_Subgroup
Provedcenter-of-group-is-normal-subgroupcenters-of-groupsnormal-subgroupsproofwiki
The center of any group is a normal subgroup of which is abelian.
Preamble
import Mathlib.GroupTheory.Subgroup.Center
Formal statement
theorem Center_of_Group_is_Normal_Subgroup (G : Type*) [Group G] : (Subgroup.center G).Normal := by sorry
Source