Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sylow.exists_subgroup_card_pow_prime

Modification history

2021-08-09 08:17
src/group_theory/sylow.lean
feat(group_theory/sylow): Generalize proof of first Sylow theorem (#8383) …
Modified sylow.exists_subgroup_card_pow_primeView on Github →
2021-03-04 13:58
src/group_theory/sylow.lean
doc(group_theory/sylow): module doc (#6477) …
Modified sylow.exists_subgroup_card_pow_primeView on Github →
2020-04-24 23:37
src/group_theory/sylow.lean
refactor(zmod): merge `zmodp` into `zmod`, use `[fact p.prime]` for tc search (#2511) …
Modified sylow.exists_subgroup_card_pow_primeView on Github →
2019-01-14 14:48
group_theory/sylow.lean
feat(group_theory/sylow): first sylow theorem (closes #591)
Added sylow.exists_subgroup_card_pow_primeView on Github →