Commit 2021-04-28 06:27 f952dd11
View on Github →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