Commit 2026-03-23 08:24 ccebd3d9

View on Github →

feat(Algebra/Group/Subgroup/Defs): merge setNormalizer into normalizer (#36852) Change Subgroup.normalizer to take in a Set G rather than a Subgroup G, and deprecate Subgroup.setNormalizer. This joins Subgroup.centralizer which is already defined on sets rather than subgroups. Subgroups can use both of them through their SetLike instance.

Estimated changes

modified theorem Subgroup.le_normalizer_map
modified theorem Subgroup.normalizer_eq_top
modified theorem Subgroup.mem_normalizer_iff
modified def Subgroup.normalizer
modified theorem Subgroup.op_normalizer
modified theorem Subgroup.unop_normalizer