Theorem ENNReal.toNNReal_ofNat

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) …
Added ENNReal.toNNReal_ofNatView on Github →