example (a : zmod 3) : zmod 2 := a

Stream: general

[Kevin Buzzard]

import data.zmod.basic

example (a : zmod 3) : zmod 2 := a

This works, and constructs a mathematically meaningless map. You can do what the heck you like with fin n as far as I am concerned, but for me this coercion is going too far. The whole point of zmod n is that it's supposed to be a mathematically meaningful ring, as opposed to fin n which is just accruing random structure and is in some sense beyond hope. What is the justification for this coercion?

[Kevin Buzzard]

I see now that the "sensible" map zmod.cast_hom is just defined via this coercion :-( so probably it's very hard to remove. Aah well.

[Eric Wieser]

(docs#zmod.cast_hom)

[Eric Wieser]

I guess docs#zmod.has_coe_t is the instance you dislike

[Eric Wieser]

I think removing the spelling via coe would be fine; that spelling should be used for canonical things. The spelling via docs#zmod.cast can continue to mean the nonsense one.

[Floris van Doorn]

It was introduced in #2511 (@Johan Commelin)

[Johan Commelin]

And in #3975 I suggest that it get removed.

[Johan Commelin]

But I haven't made time for that yet