mathlib

f9c30004 - refactor(data/finsupp/basic): split `data/finsupp/basic` into three parts (#15699)

refactor(data/finsupp/basic): split `data/finsupp/basic` into three parts (#15699) This PR splits the ~2900 lines of `data/finsupp/basic` into more manageable parts: * the most basic material (~1000 lines) moves to `data/finsupp/defs` * lemmas about `finsupp.sum` and `finsupp.prod` move to `algebra/big_operators/finsupp` * the remaining less-used definitions and lemmas remain in `data/finsupp/basic` (~1600 lines)