mathlib3

a1057a3b - feat(data/finsum): sums over sets and types with no finiteness hypotheses (#6355)

feat(data/finsum): sums over sets and types with no finiteness hypotheses (#6355) This rather large PR is mostly work of Jason KY. It is all an API for `finsum` and `finsum_in`, sums over sets with no finiteness assumption, and which return zero if the sum is infinite. Co-authored-by: Kexing <kexing.ying19@imperial.ac.uk>