basic): define `alg_hom_class` and `non_unital_alg_hom_class` (#14679)

Commit

3 years ago

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.

Author

dupuisf

Parents

5d18a722

mathlib3 2b469927 - feat(algebra/algebra/basic): define `alg_hom_class` and `non_unital_alg_hom_class` (#14679)

mathlib3
2b469927 - feat(algebra/algebra/basic): define `alg_hom_class` and `non_unital_alg_hom_class` (#14679)