feat(group_theory/sylow): the normalizer is self-normalizing (#11638)
feat(group_theory/sylow): the normalizer is self-normalizing (#11638)

with hat tip to Thomas Browning for a proof on Zuplip.





leanprover-community/mathlib,leanprover-community/mathlib