Theorem ENat.ofNat_ne_top

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

2024-02-26 00:38

Mathlib/Data/ENat/Basic.lean

chore: add lemmas for nat literals corresponding to lemmas for nat casts (#8006) …

Added ENat.ofNat_ne_top View on Github →