Cartesian product in finset

Stream: Is there code for X?

[George Shakan]

How would I write code that defines a function from X to Y where X and Y are both Cartesian product of finsets.

[Yaël Dillies]

Do you want docs#prod.map ?

[George Shakan]

hmm, I don't think so, suppose I just want to define f(x,y) = x+y. How would I go about this?

[Kyle Miller]

It would likely be helpful if you could write a #mwe showing some of what you want to define (you can put sorry where you need help)

[Yaël Dillies]

Ah, in that case you just want something like λ x : α × β, x.1 + x.2 (and maybe you can remove : α × β if Lean has enough context).

[Eric Wieser]

Is it possible you mean "finite types" instead of "finsets"?