Commit 2022-04-08 07:42 95ebbadb
View on Github →refactor(group_theory/commutator): Move commutator_le_map_commutator (#13229)
commutator_le_map_commutator is a general lemma about commutators, so it should be moved from solvable.lean to commutator.lean.