instNoetherianSpace

Mathlib.RingTheory.Spectrum.Prime.Noetherian

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

English

If R is Noetherian, then Spec(R) equipped with the Zariski topology is a Noetherian space.

Русский

Если R является Noetherian, спектр Spec(R) в топологии Зарики — это пространство Ноetherian.

LaTeX

$$$\\text{NoetherianSpace}(\\mathrm{PrimeSpectrum} R)$$$

Lean4

instance : NoetherianSpace (PrimeSpectrum R) :=
  ((noetherianSpace_TFAE <| PrimeSpectrum R).out 0 1).mpr (closedsEmbedding R).dual.wellFoundedLT

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

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

Разделы

Аффилиация

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