mk₁ — Mathlib

English

If every prime ideal is either minimal or maximal, then Krull dimension is at most 1.

Русский

Если каждый простой идеал либо минимален, либо максимален, то размерность Крull не превышает 1.

LaTeX

$$$\left( \forall I:\mathrm{Ideal}(R), I.IsPrime \rightarrow (I \in \mathrm{minimalPrimes}(R) \lor I.IsMaximal) \right) \Rightarrow \mathrm{Ring.KrullDimLE }1\;R$$

Lean4

theorem mk₁ (H : ∀ I : Ideal R, I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal) : Ring.KrullDimLE 1 R := by
  rwa [Ring.krullDimLE_one_iff]

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