instIsEmptyOfSubsingleton

Mathlib.RingTheory.Spectrum.Prime.Basic

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.instIsEmptyOfSubsingleton

← MathLib Explorer

English

If R is a subsingleton, then PrimeSpectrum R is empty.

Русский

Если R является подселтонным, спектр простых пуст.

LaTeX

$$$[\\\\Subsingleton R] ⇒ IsEmpty(PrimeSpectrum(R))$$$

Lean4

/-- The prime spectrum of the zero ring is empty. -/
instance [Subsingleton R] : IsEmpty (PrimeSpectrum R) :=
  isEmpty_iff_subsingleton.mpr inferInstance

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

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

Разделы

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

Аффилиация

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