Theorems · Theorem · combinatorics

MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero

∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_2} [Finite σ] [IsDomain R] (f : MvPolynomial σ R) (t : σ →₀ ℕ),
  MvPolynomial.coeff t f ≠ 0 →
    f.totalDegree = Finsupp.degree t →
      ∀ (S : σ → Finset R), (∀ (i : σ), t i < (S i).card) → ∃ s, (∀ (i : σ), s i ∈ S i) ∧ (MvPolynomial.eval s) f ≠ 0

The Combinatorial Nullstellensatz. Given a multi-index t : σ →₀ ℕ such that t s < (S s).card for all s, f.totalDegree = t.degree and f.coeff t ≠ 0, there exists a point x : σ → R such that x s ∈ S s for all s and f.eval s ≠ 0. [Alon_1999], theorem 2

Defined in

Mathlib.Combinatorics.Nullstellensatz

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingFiniteIsDomain