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'`.





leanprover-community/mathlib,leanprover-community/mathlib