mathlib
3aaa5647 - refactor(group_theory/commutator): Golf proof of `commutator_comm` (#12600)

Commit

3 years ago

refactor(group_theory/commutator): Golf proof of `commutator_comm` (#12600) This PR golfs the proof of `commutator_comm`.

Author

tb65536

Parents