Mathlib v3 is deprecated. Go to Mathlib v4

Theorem card_sylow_dvd_index

Modification history

2021-10-01 03:25

src/group_theory/sylow.lean

feat(group_theory/sylow): The number of Sylow subgroups equals the index of the normalizer (#9455) …

Added card_sylow_dvd_index View on Github →