coercion from `rat` to a `char_p` field

Stream: maths

[Yury G. Kudryashov]

Currently rat.cast defines coe from rat to any division_ring. Is it useful to have coercion to a division ring of non-zero characteristic?

[Alex J. Best]

Sounds useful to me!

[Yury G. Kudryashov]

When is it useful?

[Yury G. Kudryashov]

I mean, it is not a ring_hom in this case.

[Alex J. Best]

Well it's convenient right? I would like to talk about 1/2 is in zmod p. If you have a coe from int to any ring and an inv on your ring then having a/b map to a * b^(-1) seems natural.

[Yury G. Kudryashov]

Maybe you're right. Though having ↑a + ↑b not always equal to ↑(a + b) seems strange.

[Kevin Buzzard]

This sounds like a computer scientist's coercion. I'd happily have a map from $\mathbb{Z}_{(p)}$, the localisation of the integers away from the prime ideal $(p)$, to a division ring of characteristic $p$, and what the computer scientists decide to do with $1/p$ is their own business. It should be a ring homomorphism on this subset I guess.