isMaximal_iff_isPrime — Mathlib

English

In rings of Krull dimension zero, an ideal is maximal iff it is prime.

Русский

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

LaTeX

$$$I\text{ maximal} \iff I\text{ prime}$ for rings with $\mathrm{KrullDim}(R) \le 0$.$$

Lean4

theorem isMaximal_iff_isPrime [Ring.KrullDimLE 0 R] {I : Ideal R} : I.IsMaximal ↔ I.IsPrime :=
  ⟨IsMaximal.isPrime, fun _ ↦ inferInstance⟩

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