mathlib

4be58905 - fix(group_theory/subgroup/basic): generalize `centralizer` from `subgroup G` to `set G` (#18965)

fix(group_theory/subgroup/basic): generalize `centralizer` from `subgroup G` to `set G` (#18965) This is consistent with all the other `sub<foo>.centralizer` definitions. This generalization reveals that a lot of downstream results are rather strangely stated about `zpowers`. This does not attempt to change these, instead leaving the work for a follow up (either in a later mathlib3 PR or in mathlib4).