Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-31 22:22 731d93b3

View on Github →

feat(group_theory/sylow): the normalizer is self-normalizing (#11638) with hat tip to Thomas Browning for a proof on Zuplip.

Estimated changes