mathlib3
1a581ede - refactor(group_theory/solvable): Golf proof (#12552)

Commit

3 years ago

refactor(group_theory/solvable): Golf proof (#12552) This PR golfs the proof of insolvability of S_5, using the new commutator notation.

Author

tb65536

Parents