Theorem ENNReal.ofNNReal_finsetSum

Modification history

2026-06-04 10:40
Mathlib/Data/ENNReal/BigOperators.lean
feat(Data/ENNReal): more big operator lemmas (#40211) …
Added ENNReal.ofNNReal_finsetSumView on Github →