krullDimLE_one_iff — Mathlib

English

Ring Krull dimension at most 1 is equivalent to every prime ideal being either minimal or maximal.

Русский

Размерность Крull кольца R не более 1 эквивалентна тому, что каждый простой идеал является либо минимальным, либо максимальным.

LaTeX

$$$\text{Ring.KrullDimLE }1 R \iff \forall I:\mathrm{Ideal}(R), I.IsPrime \rightarrow (I \in \mathrm{minimalPrimes}(R) \lor I.IsMaximal)$$$

Lean4

theorem krullDimLE_one_iff : Ring.KrullDimLE 1 R ↔ ∀ I : Ideal R, I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal :=
  by
  simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one, Order.krullDim_le_one_iff,
    (PrimeSpectrum.equivSubtype R).forall_congr_left, Subtype.forall, PrimeSpectrum.isMax_iff, PrimeSpectrum.isMin_iff]
  rfl

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