mathlib

e15e015b - split(data/finset/sigma): Split off `data.finset.basic` (#10957)

split(data/finset/sigma): Split off `data.finset.basic` (#10957) This moves `finset.sigma` to a new file `data.finset.sigma`. I'm crediting Mario for 16d40d7491d1fe8a733d21e90e516e0dd3f41c5b