mathlib

efd9a16a - refactor(group_theory/commutator): Define commutators of subgroups in terms of commutators of elements (#12309)

refactor(group_theory/commutator): Define commutators of subgroups in terms of commutators of elements (#12309) This PR defines commutators of elements of groups. (This is one of the several orthogonal changes from https://github.com/leanprover-community/mathlib/pull/12134)