mathlib

f0f40704 - feat(topology/algebra/infinite_sum): Double sum is equal to a single value (#15157)

feat(topology/algebra/infinite_sum): Double sum is equal to a single value (#15157) A generalized version of `tsum_eq_single` that works for a double indexed sum, when all but one summand is zero. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>