finiteRingKrullDim_iff_ne_bot_and_top

English

FiniteRingKrullDim R holds iff ringKrullDim R is neither ⊥ nor ⊤.

Русский

FiniteRingKrullDim R эквивалентно тому, что ringKrullDim R не равна ни ⊥, ни ⊤.

LaTeX

$$$FiniteRingKrullDim R \\iff (ringKrullDim R \\neq \\bot \\wedge ringKrullDim R \\neq \\top)$$$

Lean4

theorem finiteRingKrullDim_iff_ne_bot_and_top : FiniteRingKrullDim R ↔ (ringKrullDim R ≠ ⊥ ∧ ringKrullDim R ≠ ⊤) :=
  (Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top (α := PrimeSpectrum R))

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