Commit 2025-10-01 08:55 e018b8de

feat(Topology/InfiniteSum): Formula for ∏' i : ι, (1 + f i) (#29857) This is the infinite version of Finset.prod_one_add. Unfortunately I think it only holds in the Summable->Multipliable direction, but not the opposite way. One usage of this is in generating power series of partition functions (infinite version of those in https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean). Using these lemma one can quickly argue about general multipliability, and direct calculation if the product factor is (1 + monomial)