Commit 2022-11-10 15:12 dfd46033

feat(algebra/*): add coercions from hom classes to their respective homs (#17000) This adds coercions from various hom classes of algebraic morphisms to their respective homs. In particular, we add these for non_unital_alg_hom_class, alg_hom_class, non_unital_star_alg_hom_class, alg_equiv_class and star_alg_hom_class. For each of these coercions, we also provided the protected simp lemma coe_coe which says that ⇑↑f = ⇑f for f a member of a hom class and ↑f its coercion to a hom.