Commit 2023-07-24 08:57 4be58905

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