mathlib3

bdfa72be - feat(group_theory/commutator): Define the set of commutators (#17276)

feat(group_theory/commutator): Define the set of commutators (#17276) With some of my upcoming group theory PRs, it is going to start being helpful to have a name for the set of commutators.