feat(group_theory/solvable): S_5 is not solvable (#7453)
This is a rather hacky proof that S_5 is not solvable. The proper proof via the simplicity of A_5 will eventually replace this. But until then, this result is needed for abel-ruffini.
Most of the work done by Jordan Brown
Co-authored-by: Thomas Browning <tb65536@uw.edu>
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
