Mathlib v3 is deprecated. Go to Mathlib v4

Theorem card_sylow_eq_index_normalizer

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_eq_index_normalizer View on Github →