Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

remove the coercion from zmod n to other rings #3975

Open
jcommelin opened this issue Aug 29, 2020 · 1 comment
Open

remove the coercion from zmod n to other rings #3975

jcommelin opened this issue Aug 29, 2020 · 1 comment

Comments

@jcommelin
Copy link
Member

We should remove the coercion, and just use zmod.cast(_hom) everywhere. The coercion causes more trouble than it is worth.
This coercion is currently used in evil ways, by coercing from zmod n to int. Here zmod.val should be used instead.

@eric-wieser
Copy link
Member

zmod.val doesn't do the right thing to get

This coercion is currently used in evil ways, by coercing from zmod n to int. Here zmod.val should be used instead.

(zmod.val x : ℤ) sends x = (-37 : zmod 0) to 37, which sounds undesirable.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

No branches or pull requests

2 participants