mathlib3

55316987 - feat(group_theory/specific_groups/dihedral): add explicit definition of center

feat(group_theory/specific_groups/dihedral): add explicit definition of center Add lemmas regarding which elements can or cannot be central and an explicit definition of the center as a subgroup. Note that the defined subgroup only coincides with the actual center of the group as long as either or , because the degenerate dihedral groups are abelian.