mathlib3

3ba1c023 - feat(group_theory/subgroup/basic): Alternate version of `mem_normalizer_iff` (#12814)

feat(group_theory/subgroup/basic): Alternate version of `mem_normalizer_iff` (#12814) This PR adds an alternate version of `mem_normalizer_iff`, in terms of commuting rather than conjugation.