Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-09 08:17 24bbbdce

View on Github →

feat(group_theory/sylow): Generalize proof of first Sylow theorem (#8383) Generalize the first proof. There is now a proof that every p-subgroup is contained in a Sylow subgroup.

Estimated changes