instDiscreteTopology

Mathlib.RingTheory.Spectrum.Prime.Noetherian

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

English

If R is Artinian, Spec(R) carries the discrete topology.

Русский

Если R Artinian, спектр Spec(R) имеет дискретную топологию.

LaTeX

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

Lean4

instance : DiscreteTopology (PrimeSpectrum R) :=
  discreteTopology_iff_finite_and_krullDimLE_zero.mpr ⟨inferInstance, inferInstance⟩

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

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

Разделы

Аффилиация

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