Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 09:31 a20032ac

View on Github →

feat(group_theory/sylow): The index of a sylow subgroup is indivisible by the prime (#14518) This PR adds a lemma stating that the index of a sylow subgroup is indivisible by the prime.

Estimated changes