height_enat — Mathlib

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 _)

Похожие утверждения