mathlib

0c9b7263 - feat(algebra/group/{pi, opposite}): add missing pi and opposite defs for `mul_hom` (#13956)

feat(algebra/group/{pi, opposite}): add missing pi and opposite defs for `mul_hom` (#13956) The declaration names and the contents of these definitions are all copied from the corresponding ones for `monoid_hom`.