Theorem ENNReal.toReal_natCast

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.toReal_natCastView on Github →