Theorem ENat.toENNReal_ofNat

Modification history

2025-01-02 08:45
Mathlib/Data/Real/ENatENNReal.lean
chore: use `ofNat()` around `Real` and `Complex` (#20388) …
Modified ENat.toENNReal_ofNatView on Github →
2023-12-04 12:41
Mathlib/Data/Real/ENatENNReal.lean
fix: add missing `no_index` around `OfNat.ofNat ` (#8317)
Modified ENat.toENNReal_ofNatView on Github →
2023-02-28 19:08
Mathlib/Data/Real/ENatENNReal.lean
feat: port Data.Real.ENatENNReal (#2529)
Added ENat.toENNReal_ofNatView on Github →