Commit 2024-05-03 08:33 2dd08f89

View on Github →

feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma (#12446) We also summable_partition (and the required Set.sigmaEquiv), needed for #10377.

Estimated changes

added theorem summable_partition