krullDimLE_iff — Mathlib

English

For any ring R, FiniteRingKrullDim R holds if and only if ringKrullDim R is not bottom and not top.

Русский

Для кольца R условие FiniteRingKrullDim R эквивалентно тому, что ringKrullDim R не равна ни нижней, ни верхней границе.

LaTeX

$$$FiniteRingKrullDim R \\;\\iff\\; (ringKrullDim R \\neq \\bot \\land ringKrullDim R \\neq \\top)$$$

Lean4

theorem krullDimLE_iff {n : ℕ} : KrullDimLE n R ↔ ringKrullDim R ≤ n :=
  Order.krullDimLE_iff n (PrimeSpectrum R)

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