vanishingIdeal_singleton — Mathlib

English

The vanishing ideal of a singleton {x} is exactly the homogeneous ideal associated to x.

Русский

VanishingIdeal от множества-одиночки {x} равен однородному идеалу, связянному с x.

LaTeX

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

Lean4

@[simp]
theorem vanishingIdeal_singleton (x : ProjectiveSpectrum 𝒜) :
    vanishingIdeal ({ x } : Set (ProjectiveSpectrum 𝒜)) = x.asHomogeneousIdeal := by simp [vanishingIdeal]

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