krullDim_eq_top_iff — Mathlib

English

Krull dim equals top iff the order is infinite dimensional.

Русский

Размерность Крулла равна ⊤ тогда и только тогда порядок бесконечно размерный.

LaTeX

$$\operatorname{krullDim}(\alpha) = \top \iff \text{InfiniteDimensionalOrder}(\alpha)$$

Lean4

theorem krullDim_eq_top_iff : krullDim α = ⊤ ↔ InfiniteDimensionalOrder α :=
  by
  refine ⟨fun h ↦ ?_, fun _ ↦ krullDim_eq_top⟩
  cases isEmpty_or_nonempty α
  · simp [krullDim_eq_bot] at h
  cases finiteDimensionalOrder_or_infiniteDimensionalOrder α
  · rw [krullDim_eq_length_of_finiteDimensionalOrder] at h
    cases h
  · infer_instance

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