Commit 2022-06-14 13:35 2b469927

View on Github →

feat(algebra/algebra/basic): define alg_hom_class and non_unital_alg_hom_class (#14679) This PR defines alg_hom_class and non_unital_alg_hom_class as part of the morphism refactor.

Estimated changes

Modified src/algebra/algebra/basic.lean

deleted theorem alg_hom.map_add

deleted theorem alg_hom.map_bit0

deleted theorem alg_hom.map_bit1

deleted theorem alg_hom.map_finsupp_prod

deleted theorem alg_hom.map_finsupp_sum

deleted theorem alg_hom.map_mul

deleted theorem alg_hom.map_multiset_prod

deleted theorem alg_hom.map_neg

deleted theorem alg_hom.map_one

deleted theorem alg_hom.map_pow

deleted theorem alg_hom.map_prod

deleted theorem alg_hom.map_smul

deleted theorem alg_hom.map_sub

deleted theorem alg_hom.map_sum

deleted theorem alg_hom.map_zero

Modified src/algebra/hom/non_unital_alg.lean

deleted theorem non_unital_alg_hom.map_add

deleted theorem non_unital_alg_hom.map_mul

deleted theorem non_unital_alg_hom.map_smul

deleted theorem non_unital_alg_hom.map_zero