Zulip Chat Archive

Stream: general

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


Kevin Buzzard (Nov 28 2021 at 13:59):

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 (Nov 28 2021 at 14:15):

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 (Nov 28 2021 at 14:53):

(docs#zmod.cast_hom)

Eric Wieser (Nov 28 2021 at 14:54):

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

Eric Wieser (Nov 28 2021 at 14:56):

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 (Nov 29 2021 at 17:13):

It was introduced in #2511 (@Johan Commelin)

Johan Commelin (Nov 29 2021 at 17:14):

And in #3975 I suggest that it get removed.

Johan Commelin (Nov 29 2021 at 17:14):

But I haven't made time for that yet


Last updated: Dec 20 2023 at 11:08 UTC