mathlib

49f5fb88 - chore(algebra/category/CommRing/limits): avoid `is_ring_hom` (#2142)

chore(algebra/category/CommRing/limits): avoid `is_ring_hom` (#2142) define a `ring_hom` instead Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>