Int to Fin

Stream: Is there code for X?

[Ka Wing Li]

It must lie in mathlib somewhere, but I cannot find a conversion of Int to Fin?

[Ruben Van de Velde]

I'm not sure that it exists

[Johan Commelin]

@Ka Wing Li Are you perhaps interested in going from Int to ZMod n?

[Eric Wieser]

open scoped Fin.CommRing will do it if you do want Fin

[Ka Wing Li]

I have come up with

import Mathlib

def Int.toFin (z : Int) (n : Nat) (hn : n ≠ 0) : Fin n :=
  ⟨z.natMod n, Int.natMod_lt hn⟩

#eval (4 : Fin 10) + (- 8 : Int) |>.toFin 10 (by trivial)

[Ka Wing Li]

Yet not so satisfying

[Kim Morrison]

You could supply an auto_param, i.e. := by lia for hn.

[Ka Wing Li]

oh nice, that does the trick

[Ka Wing Li]

Thanks!

[Eric Wieser]

Eric Wieser said:

open scoped Fin.CommRing will do it if you do want Fin

Just to be explicit, once you do this the function you want is docs#Int.cast, but this is inserted automatically as a coercion.