mathlib

cf2ff033 - feat(group_theory/sylow): Sylow subgroups are nontrivial! (#10144)

feat(group_theory/sylow): Sylow subgroups are nontrivial! (#10144) These lemmas (finally!) connect the work of @ChrisHughes24 with the recent definition of Sylow subgroups, to show that Sylow subgroups are actually nontrivial! Co-authored-by: tb65536 <tb65536@users.noreply.github.com>