mathlib

f952dd11 - refactor(algebra/big_operators/finprod, ring_theory/hahn_series): summable families now use `finsum` (#7388)

refactor(algebra/big_operators/finprod, ring_theory/hahn_series): summable families now use `finsum` (#7388) Adds a few `finprod/finsum` lemmas Uses them to refactor `hahn_series.summable_family` to use `finsum`