Commit 2022-03-12 02:28 2e7483d2
View on Github →refactor(group_theory/commutator): Move and golf commutator_le (#12599)
This PR golfs commutator_le and moves it earlier in the file so that it can be used earlier.
This PR will conflict with #12600, so don't merge them simultaneously (bors d+ might be better).