subsingleton_primeSpectrum

Mathlib.RingTheory.KrullDimension.Zero

URI: https://scilib.ai/kg/mathlib#Ring.KrullDimLE.subsingleton_primeSpectrum

← MathLib Explorer

English

In a local ring R, the prime spectrum has exactly one point.

Русский

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

LaTeX

$$Subsingleton(PrimeSpectrum(R))$$

Lean4

theorem subsingleton_primeSpectrum [IsLocalRing R] : Subsingleton (PrimeSpectrum R) :=
  ⟨fun x y ↦ PrimeSpectrum.ext <| (eq_maximalIdeal_of_isPrime x.1).trans (eq_maximalIdeal_of_isPrime y.1).symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru