mem_vanishingIdeal_singleton_iff — Mathlib

English

For a point x: σ → K, the polynomials that vanish at x form exactly the vanishing ideal of the singleton {x}. Equivalently, p lies in vanishingIdeal k {x} iff p evaluates to zero at x.

Русский

Для точки x: σ → K полиномы, которые обнуляют x, образуют ровно нулевой идеал синглтона {x}. Эквивалентно, p ∈ vanishingIdeal k {x} тогда и только тогда, когда p обнуляется при подстановке x.

LaTeX

$$$p \in \operatorname{vanishingIdeal}(k, \{x\}) \iff \ aeval_x(p) = 0$$$

Lean4

theorem mem_vanishingIdeal_singleton_iff (x : σ → K) (p : MvPolynomial σ k) :
    p ∈ (vanishingIdeal k { x } : Ideal (MvPolynomial σ k)) ↔ aeval x p = 0 :=
  ⟨fun h => h x rfl, fun hpx _ hy => hy.symm ▸ hpx⟩

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