Data.Finset.Pointwise

Stream: mathlib4

[Ruben Van de Velde]

This is big (>2500 lines) and imports a lot to define any kind of pointwise operation, as opposed to the Set side, which is split into several files. It seems like we could do something similar for Finset. @Yaël Dillies , thoughts?

[Yaël Dillies]

I have work in progress for that

[Yaël Dillies]

For the record, I dislike the way the Set files are split up and I had opened !3#17812 which was never merged