Theorem tprod_one_add

Modification history

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