mathlib3

dfd46033 - feat(algebra/*): add coercions from hom classes to their respective homs (#17000)

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.