mem_vanishingIdeal_iff — Mathlib

English

Membership in vanishingIdeal k V is equivalent to the polynomial evaluating to zero at all points of V.

Русский

Членство в vanishingIdeal эквивалентно тому, что полином равен нулю во всех точках V.

LaTeX

$$$p \\in \\mathrm{vanishingIdeal}(k,V) \\iff \\forall x\\in V,\\; aeval(x,p)=0$$$

Lean4

@[simp]
theorem mem_vanishingIdeal_iff {V : Set (σ → K)} {p : MvPolynomial σ k} :
    p ∈ vanishingIdeal k V ↔ ∀ x ∈ V, aeval x p = 0 :=
  Iff.rfl

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