eq_maximalIdeal_of_isPrime — Mathlib

English

Let R be a local ring (IsLocalRing R) with Krull dimension ≤ 0. Then every prime ideal J of R is equal to the unique maximal ideal of R.

Русский

Пусть R — локальное кольцо (IsLocalRing R) с размерностью Крull не выше нуля. Тогда любой простый идеал J кольца R равен единственному максимальному идеалу R.

LaTeX

$$$\\forall J:\\mathord{\\mathsf{Ideal}}(R),\\; [J.IsPrime]\\; \\Rightarrow\\; J = \\operatorname{maximalIdeal}R$$$

Lean4

theorem eq_maximalIdeal_of_isPrime [IsLocalRing R] (J : Ideal R) [J.IsPrime] : J = IsLocalRing.maximalIdeal R :=
  (((Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 1 rfl rfl).mp ⟨‹_›, ‹_›⟩).unique ‹_› inferInstance

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