Theorems · Theorem · combinatorics

MvPolynomial.eq_zero_of_eval_zero_at_prod_finset

∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (P : MvPolynomial σ R) (S : σ → Finset R),
  (∀ (i : σ), MvPolynomial.degreeOf i P < (S i).card) →
    (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (MvPolynomial.eval x) P = 0) → P = 0

A multivariate polynomial that vanishes on a large product finset is the zero polynomial.

Defined in

Mathlib.Combinatorics.Nullstellensatz

Cited by

1 results in Mathlib

Foundations

Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFiniteIsDomain