mathlib3

1e560a67 - refactor(group_theory/commutator): Generalize `map_commutator_element` (#12555)

refactor(group_theory/commutator): Generalize `map_commutator_element` (#12555) This PR generalizes `map_commutator_element` from `monoid_hom_class F G G` to `monoid_hom_class F G G'`.