is_ring_hom instead of cast_mul

Stream: general

[Chris Hughes]

What's the reason not to mark coe as a ring_hom instead of using int.cast_mul and stuff like that?

[Mario Carneiro]

Well, for one thing ring_hom didn't exist when cast was written

[Mario Carneiro]

but ring_hom.mul is not applicable as a simp lemma for reasons that have been discussed before, so we would still want int.cast_mul in any case

[Mario Carneiro]

But it's reasonable to prove that coe is a ring_hom given the existing theorems