mathlib

13c6c437 - feat(group_theory/subgroup/basic): Centralizer of closure is intersection of centralizers (#16394)

feat(group_theory/subgroup/basic): Centralizer of closure is intersection of centralizers (#16394) This PR adds some more API for `subgroup.centralizer` and proves that the centralizer of a closure is the intersection of the centralizers.