Theorem multipliable_one_add_of_summable_prod

Modification history

2025-10-01 08:55
Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
feat(Topology/InfiniteSum): Formula for `∏' i : ι, (1 + f i)` (#29857) …
Added multipliable_one_add_of_summable_prodView on Github →