{hom,prod}): has_mul and mul_hom.prod (#12110)

Commit

3 years ago

feat(algebra/group/{hom,prod}): has_mul and mul_hom.prod (#12110) Ported over from `monoid_hom`.

Author

pechersky

Parents