Def ENat.toENNReal

Modification history

2024-12-20 13:13

Mathlib/Data/Real/ENatENNReal.lean

feat: add `ENat.map` and lemmas (#19149)

Modified ENat.toENNReal View on Github →

2023-02-28 19:08

Mathlib/Data/Real/ENatENNReal.lean

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

Added ENat.toENNReal View on Github →