Commit 2021-10-01 03:25 125dac81

View on Github →

feat(group_theory/sylow): The number of Sylow subgroups equals the index of the normalizer (#9455) This PR adds further consequences of Sylow's theorems (still for infinite groups, more will be PRed later).

Estimated changes

Modified src/group_theory/sylow.lean

added theorem card_sylow_dvd_index

added theorem card_sylow_eq_card_quotient_normalizer

added theorem card_sylow_eq_index_normalizer

added theorem sylow.orbit_eq_top

added theorem sylow.stabilizer_eq_normalizer