Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_hom.coe_mul

Modification history

2022-02-22 22:49
src/algebra/group/pi.lean
feat(algebra/group/{hom,prod}): has_mul and mul_hom.prod (#12110) …
Added mul_hom.coe_mulView on Github →