Def ENNReal.some

Modification history

2023-11-09 10:14

Mathlib/Data/Real/ENNReal.lean

chore(Data/Real/ENNReal): rename `some` to `ofNNReal` (#8276) …

Deleted ENNReal.some View on Github →

2023-02-27 08:10

Mathlib/Data/Real/ENNReal.lean

feat: port Data.Real.ENNReal (#2388) …

Added ENNReal.some View on Github →