mem_minimalPrimes_iff_isPrime — Mathlib

English

In rings of Krull dimension zero, I is in minimalPrimes(R) iff I is prime.

Русский

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

LaTeX

$$$I\in \mathrm{minimalPrimes}(R) \iff I\text{ IsPrime}$$$

Lean4

theorem mem_minimalPrimes_iff_isPrime [Ring.KrullDimLE 0 R] {I : Ideal R} : I ∈ minimalPrimes R ↔ I.IsPrime :=
  ⟨(·.1.1), fun _ ↦ I.mem_minimalPrimes_of_krullDimLE_zero⟩

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