Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 22:49 2ab3e2fa

View on Github →

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

Estimated changes

added theorem mul_hom.comp_mul
added theorem mul_hom.mul_apply
added theorem mul_hom.mul_comp
added theorem mul_hom.coe_mul
added theorem mul_hom.coe_fst
added theorem mul_hom.coe_prod
added theorem mul_hom.coe_prod_map
added theorem mul_hom.coe_snd
added theorem mul_hom.comp_coprod
added def mul_hom.coprod
added theorem mul_hom.coprod_apply
added def mul_hom.fst
added theorem mul_hom.fst_comp_prod
added theorem mul_hom.prod_apply
added def mul_hom.prod_map
added theorem mul_hom.prod_map_def
added theorem mul_hom.prod_unique
added def mul_hom.snd
added theorem mul_hom.snd_comp_prod