mathlib
a20032ac - feat(group_theory/sylow): The index of a sylow subgroup is indivisible by the prime (#14518)

Commit

3 years ago

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.

Author

tb65536

Parents

54236f5a

mathlib a20032ac - feat(group_theory/sylow): The index of a sylow subgroup is indivisible by the prime (#14518)

mathlib
a20032ac - feat(group_theory/sylow): The index of a sylow subgroup is indivisible by the prime (#14518)