Theorem HasProd.nonneg

Modification history

2026-08-03 20:51
Mathlib/Topology/Algebra/InfiniteSum/Order.lean
feat(Topology/InfiniteSum): non-negativity of tprod (#42184)
Added HasProd.nonnegView on Github →