Theorem NNReal.coe_prod

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_prod View on Github →

2023-02-20 08:04

Mathlib/Data/Real/NNReal.lean

feat: port Data.Real.NNReal (#2234)

Added NNReal.coe_prod View on Github →