feat(group_theory/perm/*): Generating S_n (#7211)
This PR proves several lemmas about generating S_n, culminating in the following result:
If H is a subgroup of S_p, and if H has cardinality divisible by p, and if H contains a transposition, then H is all of S_p.
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
