Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-26 13:29 2b257230

View on Github →

feat(group_theory/sylow): add characteristic_of_normal (#11636) A normal sylow subgroup is characteristic.

Estimated changes