cartesian product

Stream: Is there code for X?

[George Shakan]

How can I create the Cartesian product in finsets. I thought it should be in data.finset.pi and pi A B for finsets A,B, but I am getting a type error I do not really understand

[Johan Commelin]

finset.product

[Johan Commelin]

So if you have s : finset X and t : finset Y, then you can write s.product t to get a finset (X × Y).

[George Shakan]

That works for prod A B, but when I try for prod (A+B) C it does not and does not like A+B

[George Shakan]

(Here A+B is the sumset)