mathlib3

050404af - feat(group_theory/sylow): Sylow subgroups are Hall subgroups (#14624)

feat(group_theory/sylow): Sylow subgroups are Hall subgroups (#14624) This PR adds a lemma stating that Sylow subgroups are Hall subgroups (cardinality is coprime to index).