Theorem ENat.toENNReal_ofNat

Modification history

2023-12-04 12:41

Mathlib/Data/Real/ENatENNReal.lean

fix: add missing `no_index` around `OfNat.ofNat ` (#8317)

Modified ENat.toENNReal_ofNat View on Github →

2023-02-28 19:08

Mathlib/Data/Real/ENatENNReal.lean

feat: port Data.Real.ENatENNReal (#2529)

Added ENat.toENNReal_ofNat View on Github →