mathlib3

c2e78d27 - refactor(data/zmod): generalize zmod.cast_hom (#2900)

refactor(data/zmod): generalize zmod.cast_hom (#2900) Currently, `zmod.cast_hom` would cast `zmod n` to rings `R` of characteristic `n`. This PR builds `cast_hom` for rings `R` with characteristic `m` that divides `n`.