mathlib

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

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).