Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_hom.prod_map

Modification history

2022-04-20 18:42
src/algebra/group/prod.lean
feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526) …
Modified mul_hom.prod_mapView on Github →
2022-02-22 22:49
src/algebra/group/prod.lean
feat(algebra/group/{hom,prod}): has_mul and mul_hom.prod (#12110) …
Added mul_hom.prod_mapView on Github →