Theorem ENat.some_eq_coe

Modification history

2026-07-17 11:15

Mathlib/Data/ENat/Basic.lean

chore(Data/ENat): replace `coe` with `natCast` in lemma names (#41140) …

Deleted ENat.some_eq_coe View on Github →

2023-04-10 11:19

Mathlib/Data/ENat/Basic.lean

feat: port Order.Height (#2186)

Added ENat.some_eq_coe View on Github →