Mathlib v3 is deprecated. Go to Mathlib v4

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 def Magma.of_hom
modified theorem Magma.of_hom_apply
modified def Semigroup.of_hom
modified theorem Semigroup.of_hom_apply
modified theorem mul_hom.map_dvd
modified def free_magma.lift
modified theorem free_magma.lift_aux_unique
modified def mul_hom.single
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 structure mul_equiv
modified def mul_hom.inverse
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
modified def set.singleton_mul_hom
modified def mul_hom.eq_mlocus
modified theorem mul_hom.eq_of_eq_on_mdense
modified theorem mul_hom.eq_of_eq_on_mtop
modified theorem mul_hom.eq_on_mclosure
modified def nhds_mul_hom