zeroLocus_singleton_one

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology

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

English

The vanishing locus of the singleton set {1} is empty.

Русский

Множество нулей для одиночного элемента 1 пусто.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}(\{1\}) = \emptyset $$$

Lean4

@[simp]
theorem zeroLocus_singleton_one : zeroLocus 𝒜 ({ 1 } : Set A) = ∅ :=
  zeroLocus_empty_of_one_mem 𝒜 (Set.mem_singleton (1 : A))

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

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

Разделы

Аффилиация

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