krullDim_eq_length_of_finiteDimensionalOrder

English

If α is infinitely dimensional, the Krull dimension equals top.

Русский

Если α бесконечно размерна, то размерность Крулла равна ⊤.

LaTeX

$$\operatorname{krullDim}(\alpha) = \top$$

Lean4

theorem krullDim_eq_length_of_finiteDimensionalOrder [FiniteDimensionalOrder α] :
    krullDim α = (LTSeries.longestOf α).length :=
  le_antisymm
      (iSup_le <| fun _ ↦
        WithBot.coe_le_coe.mpr <| WithTop.coe_le_coe.mpr <| RelSeries.length_le_length_longestOf _ _) <|
    le_iSup (fun (i : LTSeries _) ↦ (i.length : WithBot (WithTop ℕ))) <| LTSeries.longestOf _

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