mathlib

2e7483d2 - refactor(group_theory/commutator): Move and golf `commutator_le` (#12599)

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).