mathlib3

45ef183d - feat(group_theory/subgroup/basic): The center can be written as the intersection of centralizers (#16837)

feat(group_theory/subgroup/basic): The center can be written as the intersection of centralizers (#16837) This PRs adds a lemma that writes the center as the intersection of centralizers. I kept `S` explicit so that you can `rw center_eq_infi S` (specifying `S` without having to immediately supply a proof of `hS`).