mathlib3

3e2fb4c7 - feat(data/rat/cast): generalize `ext` lemmas (#16268)

feat(data/rat/cast): generalize `ext` lemmas (#16268) * generalize `monoid_with_zero_hom.ext_rat` to `monoid_with_zero`; * deduce `ext` lemma for `ring_hom`s from `monoid_with_zero_hom` version; * use hom classes.