mathlib3

6687cf15 - feat(group_theory/sylow): `fintype (sylow p H)` from `fintype (sylow p G)` (#11664)

feat(group_theory/sylow): `fintype (sylow p H)` from `fintype (sylow p G)` (#11664) If the number of Sylow `p`-subgroups of `G` is finite, then the number of Sylow `p`-subgroups of `H` is finite.