mk₀ — Mathlib

English

If every prime ideal is maximal, then Ring.KrullDimLE 0 R holds.

Русский

Если для каждого простого идеала выполняется тождество максимальности, то Ring.KrullDimLE 0 R выполняется.

LaTeX

$$$\\forall I: \\text{Ideal } R, I.IsPrime \\to I.IsMaximal \\Rightarrow Ring.KrullDimLE 0 R$$$

Lean4

theorem mk₀ (H : ∀ I : Ideal R, I.IsPrime → I.IsMaximal) : Ring.KrullDimLE 0 R := by rwa [Ring.krullDimLE_zero_iff]

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