subset_zeroLocus_vanishingIdeal

Mathlib.RingTheory.Spectrum.Prime.Basic

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

English

For any t, t ⊆ zeroLocus(vanishingIdeal(t)).

Русский

Для любого набора t выполняется t ⊆ zeroLocus(vanishingIdeal(t)).

LaTeX

$$$ t \subseteq \operatorname{zeroLocus}(\operatorname{vanishingIdeal}(t)) $$$

Lean4

theorem subset_zeroLocus_vanishingIdeal (t : Set (PrimeSpectrum R)) : t ⊆ zeroLocus (vanishingIdeal t) :=
  (gc R).l_u_le t

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

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

Разделы

Аффилиация

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