mem_minimalPrimes_of_krullDimLE_zero

English

For prime ideals I in rings with Krull dimension at most zero, I lies in the set of minimal primes.

Русский

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

LaTeX

$$$[\mathrm{Ring.KrullDimLE}\;0\;R](I) \Rightarrow I\in \mathrm{minimalPrimes}(R)$$$

Lean4

theorem mem_minimalPrimes_of_krullDimLE_zero [Ring.KrullDimLE 0 R] (I : Ideal R) [I.IsPrime] : I ∈ minimalPrimes R :=
  minimalPrimes_eq_minimals (R := R) ▸ ⟨‹_›, fun J hJ hJI ↦ (IsMaximal.eq_of_le inferInstance IsPrime.ne_top' hJI).ge⟩

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