Theorem ENNReal.toNNReal_nat

Modification history

2025-02-19 10:31
Mathlib/Data/ENNReal/Basic.lean
chore: rename ENNReal.to{NN}Real_nat -> ENNReal.to{NN}Real_natCast (#22071) …
Deleted ENNReal.toNNReal_natView on Github →
2023-02-27 08:10
Mathlib/Data/Real/ENNReal.lean
feat: port Data.Real.ENNReal (#2388) …
Added ENNReal.toNNReal_natView on Github →