mathlib3

93fbab6d - feat(data/finsupp/big_operators): sum of finsupp and their support (#15155)

feat(data/finsupp/big_operators): sum of finsupp and their support (#15155) With some additional API for pairwise on multisets and coerced lists On the way to computable list-based polynomials Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>