height_last_longestOf — Mathlib

English

For finite dimensional α, the height of the last element of the longest LTSeries equals krullDim α.

Русский

Для конечной размерности α высота последнего элемента самой длинной LTSeries равна размерности Крулла.

LaTeX

$$height((\mathrm{LTSeries.longestOf}(\alpha)).last) = \operatorname{krullDim}(\alpha)$$

Lean4

@[simp]
theorem _root_.LTSeries.height_last_longestOf [FiniteDimensionalOrder α] :
    height (LTSeries.longestOf α).last = krullDim α :=
  by
  refine le_antisymm (height_le_krullDim _) ?_
  rw [krullDim_eq_length_of_finiteDimensionalOrder, height]
  norm_cast
  exact le_iSup_iff.mpr <| fun _ h ↦ iSup_le_iff.mp (h _) le_rfl

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