Commit 2025-12-26 17:40 1544615b
View on Github →feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered (#30436)
This extends the existing Finset.prod_one_sub_ordered to infinite sum/product, and also adds the more natural add version.
Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed.