isMaximal' — Mathlib

English

In rings of Krull dimension zero, a prime ideal is maximal.

Русский

В кольцах с размерностью Крull равной нулю простой идеал является максимальным.

LaTeX

$$$\forall I:\mathrm{Ideal}(R),\; I\text{ prime }\Rightarrow I\text{ maximal}$ under the assumption $\mathrm{KrullDim}(R) \le 0$.$$

Lean4

/-- Also see `Ideal.IsPrime.isMaximal` for the analogous statement for Dedekind domains. -/
theorem isMaximal' [Ring.KrullDimLE 0 R] {I : Ideal R} (hI : I.IsPrime) : I.IsMaximal :=
  I.isMaximal_of_isPrime

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