unique_of_ringKrullDimLE_zero — Mathlib

English

In a local ring R, PrimeSpectrum R is a unique set; there is a single prime ideal.

Русский

В локальном кольце R спектр простых идеалов состоит из единственного элемента.

LaTeX

$$Unique(PrimeSpectrum(R))$$

Lean4

instance unique_of_ringKrullDimLE_zero [IsLocalRing R] : Unique (PrimeSpectrum R) :=
  ⟨⟨IsLocalRing.closedPoint _⟩, fun _ ↦ PrimeSpectrum.ext (Ring.KrullDimLE.eq_maximalIdeal_of_isPrime _)⟩

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