finite cyclic structure

Stream: maths

[Alex Kontorovich]

Here's a structural question: suppose I have a map f say from Z/7 to some Type X (it's important for the application to have a cyclic structure for the domain), and I want to make a map g from Z/3 to X by setting g 0 = f 2, g 1 = f 4, and g 2 = f 5 (or whatever). More generally I want to be able to define maps between finite cyclic (or totally ordered) sets. Does Lean have a good structure for that? Thanks!

[Kevin Buzzard]

You don't say what you mean by Z/7 but if you mean fin 7 then there is some API for this; you just need a map from fin 3 to fin 7 and you can use vector notation for this.

[Anatole Dedecker]

I guess "it is important to have a cyclic structure" means that it has to be docs#zmod right?

[Anatole Dedecker]

Fortunately docs#zmod is (almost always) defeq to docs#fin so you can do what Kevin says

[Alex Kontorovich]

Oh Fin 7 already has the structure of ZMod 7? How can I combine vector notation with abstract things? For example, if f is a map from ZMod n to X and i < j < n, and I want to make a map g from ZMod (j-i) to X by setting g k = f (k+i), except if k=5, in which case I want it to be f 0. Or something like that. I suppose I answered my own question, as long as I really can replace ZMod's above with Fin...? Thanks!

[Adam Topaz]

You can always use if then else.