Commit 2022-03-11 06:12 355472dc
View on Github →refactor(group_theory/commutator): Golf proof of commutator_mem_commutator (#12584)
This PR golfs the proof of commutator_mem_commutator, and moves it earlier in the file so that it can be used earlier.