Theorem ENNReal.coe_mono

Modification history

2023-11-09 10:14

Mathlib/Data/Real/ENNReal.lean

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

Modified ENNReal.coe_mono View on Github →

2023-02-27 08:10

Mathlib/Data/Real/ENNReal.lean

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

Added ENNReal.coe_mono View on Github →