mathlib3

24bbbdce - feat(group_theory/sylow): Generalize proof of first Sylow theorem (#8383)

feat(group_theory/sylow): Generalize proof of first Sylow theorem (#8383) Generalize the first proof. There is now a proof that every p-subgroup is contained in a Sylow subgroup. Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>