isMaximal_of_isPrime — Mathlib

English

If R is a ring with Krull dimension zero, then every prime ideal of R is maximal.

Русский

Если кольцо R имеет размерность Крull нулевой, то каждый простой (prime) идеал R является максимальным.

LaTeX

$$$\text{KrullDim}(R) \le 0 \;\Longrightarrow\; \forall I:\mathrm{Ideal}(R),\; \mathrm{Prime}(I) \Rightarrow \mathrm{Maximal}(I)$.$$

Lean4

theorem isMaximal_of_isPrime [Ring.KrullDimLE 0 R] (I : Ideal R) [I.IsPrime] : I.IsMaximal :=
  Ring.krullDimLE_zero_iff.mp ‹_› I ‹_›

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