Commit 2022-10-11 09:55 45ef183d

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).