Theorem NNReal.coe_sum

Modification history

2024-05-27 08:32
Mathlib/Data/Real/NNReal.lean
chore: Use the new `∑ i ∈ s, f i` notation (#13209) …
Modified NNReal.coe_sumView on Github →
2023-02-20 08:04
Mathlib/Data/Real/NNReal.lean
feat: port Data.Real.NNReal (#2234)
Added NNReal.coe_sumView on Github →