Theorem ENat.map_ofNat

Modification history

2025-01-07 09:21

Mathlib/Data/ENat/Basic.lean

chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) …

Modified ENat.map_ofNat View on Github →

2024-12-20 13:13

Mathlib/Data/ENat/Basic.lean

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

Added ENat.map_ofNat View on Github →