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.

Estimated changes

Modified src/algebra/group/opposite.lean

added def add_hom.mul_op

added def add_hom.mul_unop

added def mul_hom.from_opposite

added def mul_hom.op

added def mul_hom.to_opposite

added def mul_hom.unop

Modified src/algebra/group/pi.lean

added def mul_hom.coe_fn

added def pi.const_mul_hom

added def pi.eval_mul_hom