homogeneousIdeal_le_vanishingIdeal_zeroLocus

English

If I is a homogeneous ideal, then I is contained in the vanishing ideal of the zero locus of I.

Русский

Если I — однородный идеал, то I содержится в vanishingIdeal нулевой области нулевой локации I.

LaTeX

$$$I \\le \\mathrm{vanishingIdeal}(\\mathrm{zeroLocus} 𝒜 I).$$$

Lean4

theorem homogeneousIdeal_le_vanishingIdeal_zeroLocus (I : HomogeneousIdeal 𝒜) : I ≤ vanishingIdeal (zeroLocus 𝒜 I) :=
  (gc_homogeneousIdeal _).le_u_l I

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