Theorem tprod_nonneg

Modification history

2026-08-03 20:51

Mathlib/Topology/Algebra/InfiniteSum/Order.lean

feat(Topology/InfiniteSum): non-negativity of tprod (#42184)

Added tprod_nonneg View on Github →