Commit 2022-09-07 15:10 13c6c437
View on Github →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.