mathlib

6a5a2b13 - feat(data/rat/cast): drop an unneeded typeclass assumption (#15972)

feat(data/rat/cast): drop an unneeded typeclass assumption (#15972) * drop `[char_zero _]` assumption in `map_rat_cast`; * golf `ring_hom.eq_rat_cast`, generalize to `ring_hom_class`.