English
For any ENat element n, the height function returns n itself. In other words, height(n) = n for n ∈ ENat.
Русский
Для любого элемента n из ENат высота равна самому n: height(n) = n.
LaTeX
$$$\\forall n \\in \\mathbb{N}_\\infty,\\; \\operatorname{height}(n) = n$$$
Lean4
@[simp]
theorem height_enat (n : ℕ∞) : height n = n := by
cases n with
| top => simp only [← WithBot.coe_eq_coe, height_top_eq_krullDim, krullDim_enat, WithBot.coe_top]
| coe n => exact (height_coe_withTop _).trans (height_nat _)