Theorem hasProd_one_add_of_hasSum_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 hasProd_one_add_of_hasSum_prodView on Github →