mathlib3

876ef05e - feat(group_theory/commutator): Add `commutator_element_self` (#16437)

feat(group_theory/commutator): Add `commutator_element_self` (#16437) This PR adds `commutator_element_self`, similar to `commutator_element_one_left` and `commutator_element_one_right`.