Commit 2022-05-05 03:36 0c9b7263
View on Github →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
.