Commit 2022-04-20 18:42 242d6875

View on Github →

feat(algebra/hom/group and *): introduce mul_hom M N notation M →ₙ* N (#13526) The discussion and poll related to this new notation can be found in this Zulip thread

Estimated changes

modified theorem mul_hom.coe_prod
modified def mul_hom.coprod
modified def mul_hom.fst
modified theorem mul_hom.fst_comp_prod
modified theorem mul_hom.prod_apply
modified theorem mul_hom.prod_comp_prod_map
modified def mul_hom.prod_map
modified theorem mul_hom.prod_unique
modified def mul_hom.snd
modified theorem mul_hom.snd_comp_prod
modified def mul_mul_hom
modified def with_one.coe_mul_hom
modified def with_one.lift
modified def with_one.map
modified theorem with_one.map_coe
modified theorem with_one.map_comp
modified theorem with_one.map_map
modified theorem mul_hom.coe_inj
modified theorem mul_hom.ext
modified theorem mul_hom.ext_iff
modified def mul_hom.id
modified theorem mul_hom.to_fun_eq_coe