Theorem Finset.prod_one_add_ordered

Modification history

2025-12-26 17:40
Mathlib/Algebra/BigOperators/Ring/Finset.lean
feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered (#30436) …
Added Finset.prod_one_add_orderedView on Github →