## Stream: maths

### Topic: coercion from rat to a char_p field

#### Yury G. Kudryashov (Apr 09 2020 at 18:06):

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 (Apr 09 2020 at 18:19):

Sounds useful to me!

#### Yury G. Kudryashov (Apr 09 2020 at 18:25):

When is it useful?

#### Yury G. Kudryashov (Apr 09 2020 at 18:25):

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

#### Alex J. Best (Apr 09 2020 at 18:29):

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 (Apr 09 2020 at 18:33):

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

#### Kevin Buzzard (Apr 09 2020 at 19:12):

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.

Last updated: May 10 2021 at 08:14 UTC