Commit 2021-06-21 19:43 520bbe69

View on Github →

feat(algebra/non_unital_alg_hom): define non_unital_alg_hom (#7863) The motivation is to be able to state the universal property for a magma algebra using bundled morphisms.

Estimated changes

Created src/algebra/non_unital_alg_hom.lean

added theorem alg_hom.coe_to_non_unital_alg_hom

added def alg_hom.to_non_unital_alg_hom

added theorem alg_hom.to_non_unital_alg_hom_eq_coe

added theorem non_unital_alg_hom.coe_comp

added theorem non_unital_alg_hom.coe_distrib_mul_action_hom_mk

added theorem non_unital_alg_hom.coe_injective

added theorem non_unital_alg_hom.coe_inverse

added theorem non_unital_alg_hom.coe_mk

added theorem non_unital_alg_hom.coe_mul_hom_mk

added theorem non_unital_alg_hom.coe_one

added theorem non_unital_alg_hom.coe_to_distrib_mul_action_hom

added theorem non_unital_alg_hom.coe_to_mul_hom

added theorem non_unital_alg_hom.coe_zero

added def non_unital_alg_hom.comp

added theorem non_unital_alg_hom.comp_apply

added theorem non_unital_alg_hom.ext

added theorem non_unital_alg_hom.ext_iff

added def non_unital_alg_hom.inverse

added theorem non_unital_alg_hom.map_add

added theorem non_unital_alg_hom.map_mul

added theorem non_unital_alg_hom.map_smul

added theorem non_unital_alg_hom.map_zero

added theorem non_unital_alg_hom.mk_coe

added theorem non_unital_alg_hom.one_apply

added theorem non_unital_alg_hom.to_distrib_mul_action_hom_eq_coe

added theorem non_unital_alg_hom.to_fun_eq_coe

added theorem non_unital_alg_hom.to_mul_hom_eq_coe

added theorem non_unital_alg_hom.zero_apply

added structure non_unital_alg_hom