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





leanprover-community/mathlib,leanprover-community/mathlib