vanishingIdeal_univ

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

URI: https://scilib.ai/kg/mathlib#ProjectiveSpectrum.vanishingIdeal_univ

English

The vanishing ideal of the empty set is the top element (the whole ring).

Русский

VanishingIdeal пустого множества равен вершине (целый колд в кольце).

LaTeX

$$$$ \\operatorname{vanishingIdeal}(\\varnothing) = \\top $$$$

Lean4

@[simp]
theorem vanishingIdeal_univ : vanishingIdeal (∅ : Set (ProjectiveSpectrum 𝒜)) = ⊤ := by simpa using (gc_ideal _).u_top

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

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

Разделы

Аффилиация

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