Splitting up algebra.pointwise

Stream: general

[Yaël Dillies]

Are people in favor of splitting up file#algebra/pointwise? #12694 adds 140 lines (for a total of 1.5k) and my next PR will add ~600 lines of finset operations.

The one way I see we could split it up is into

• algebra.pointwise.finset
• algebra.pointwise.set

Feel free to come up with better!

[Bhavik Mehta]

I'm in favour of this

[Eric Wieser]

I think a lot of the existing imports will only need the set version, so that seems like a good split to me

[Floris van Doorn]

Since we also have order.filter.pointwise (and various others), how about doing the same split, but moving them to data.set.pointwise and data.finset.pointwise?

[Yaël Dillies]

Yeah why not!

[Yaël Dillies]

While we're at it, I just noticed file#algebra/algebra/operations. Shouldn't it be called algebra.algebra.pointwise?

[Yaël Dillies]

#12831