vanishingIdeal_singleton

Mathlib.RingTheory.Spectrum.Prime.Basic

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

← MathLib Explorer

English

The vanishing ideal of a singleton {x} equals x.asIdeal.

Русский

vanishingIdeal({x}) = x.asIdeal.

LaTeX

$$$\\\\operatorname{vanishingIdeal}(\\\\{ x \\\\} ) = x.asIdeal$$$

Lean4

@[simp]
theorem vanishingIdeal_singleton (x : PrimeSpectrum R) : vanishingIdeal ({ x } : Set (PrimeSpectrum R)) = x.asIdeal :=
  by simp [vanishingIdeal]

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

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

Разделы

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

Аффилиация

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