Theorem ENNReal.coe_finsetSum

Modification history

2026-06-04 10:40
Mathlib/Data/ENNReal/BigOperators.lean
feat(Data/ENNReal): more big operator lemmas (#40211) …
Deleted ENNReal.coe_finsetSumView on Github →
2026-04-26 16:26
Mathlib/Data/ENNReal/BigOperators.lean
chore: camel-case `finset_sum` in lemma names (#37793) …
Added ENNReal.coe_finsetSumView on Github →