mathlib3

9114ddff - chore(data/set/pointwise/basic): split (#17768)

chore(data/set/pointwise/basic): split (#17768) Split off new files `data/set/pointwise/smul` and `data/set/pointwise/finite` from `data/set/pointwise/basic`, reducing imports of the basic file.