mathlib3

c9fe6d1a - feat(algebra/algebra): instantiate `ring_hom_class` for `alg_hom` (#10853)

feat(algebra/algebra): instantiate `ring_hom_class` for `alg_hom` (#10853) This PR provides a `ring_hom_class` instance for `alg_hom`, to be used in #10783. I'm not quite finished with my design of morphism classes for linear maps, but I expect this instance will stick around anyway: to avoid a dangerous instance `alg_hom_class F R A B → ring_hom_class F A B` (where the base ring `R` can't be inferred), `alg_hom_class` will probably have to be unbundled and take a `ring_hom_class` as a parameter.