mathlib3

198cb64d - refactor(ring_theory): generalize basic API of `ring_hom` to `ring_hom_class` (#14756)

refactor(ring_theory): generalize basic API of `ring_hom` to `ring_hom_class` (#14756) This PR generalizes part of the basic API of ring homs to `ring_hom_class`. This notably includes things like `ring_hom.ker`, `ideal.map` and `ideal.comap`. I left the namespaces unchanged, for example `ring_hom.ker` remains the same even though it is now defined for any `ring_hom_class` morphism; this way dot notation still (mostly) works for actual ring homs.