Commit 2022-03-04 17:34 efd9a16a
View on Github →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)