Different casts from zmod

Stream: Is there code for X?

[Heather Macbeth]

How do I prove that cast of cast equals cast, coming out of zmod?

import data.zmod.basic
import data.complex.basic

example {m : ℕ} (i : zmod m) : ((i:ℝ):ℂ) = (i:ℂ) := sorry

[Johan Commelin]

That cast should really die.

[Johan Commelin]

There should be a lemma saying that ((i:int):R) = (i:R) for char 0 rings R.

[Johan Commelin]

example {m : ℕ} (i : zmod m) : ((i:ℝ):ℂ) = (i:ℂ) :=
begin
  conv {
    rw [← zmod.int_cast_comp_cast],
    to_rhs,
    rw [← zmod.int_cast_comp_cast] },
  norm_cast,
end

[Heather Macbeth]

Thanks!

[Eric Wieser]

Are we just missing some norm_cast attributes?

[Johan Commelin]

@Eric Wieser I'm not a norm_cast expert, but zmod.int_cast_comp_cast will loop if you apply it in the \l direction.

[Johan Commelin]

(That's why I have the complicated conv { rw, to_rhs, rw } construction.

[Kevin Buzzard]

This thread is making my stomach hurt. Why do we even have casts from Z/mZ to R or C? Why would I expect the example to be true? It's not mathematically meaningful. There are monoid homs from Z/mZ to C taking values in 0 union roots of unity which I could imagine in a parallel universe were used as casts, and then the example would be false.

[Eric Wieser]

Attempting a doc link: docs#zmod.cast

[Johan Commelin]

Johan Commelin said:

That cast should really die.

I stand by my point.

[Eric Wieser]

That cast is piggy-backing on a similar cast that fin n has (edit: fin.val is not zmod.val)

[Eric Wieser]

But maybe that one isn't so bad because at least fin is morally positive in some sense, at least when you ignore addition

[Johan Commelin]

We can protect ourselves by assuming char_p R n for the cast. Then it will only show up in sensible places.

[Eric Wieser]

That's probably safe, although the cast is also valid when n=0

[Johan Commelin]

Yes, there is a meaningful cast zmod n -> R when char_p R m and m | n.

[Johan Commelin]

But I wouldn't mind having no cast at all, and just using docs#zmod.cast_hom instead.