schwartz_zippel_exists_nonzero_eval

theoremverified

Let F be an integral domain, p a nonzero polynomial in n variables over F, and S a nonempty finite subset of F. If the total degree of p is less than the cardinality of S, then there is a point x in S^n at which p does not vanish. Equivalently, a nonzero polynomial of total degree d is not the zero function on S^n, so random evaluation from S^n detects nonzeroness.

Statement

theorem schwartz_zippel_exists_nonzero_eval {F : Type*} [CommRing F] [IsDomain F] [DecidableEq F]
    {n : ℕ} {p : MvPolynomial (Fin n) F} (hp : p ≠ 0) {S : Finset F} (hS : 0 < S.card)
    (hd : p.totalDegree < S.card) :
    ∃ x ∈ Fintype.piFinset (fun _ : Fin n => S), MvPolynomial.eval x p ≠ 0

Source: Schwartz 1980 / Zippel 1979 (probabilistic polynomial identity testing); Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean (`MvPolynomial.schwartz_zippel_totalDegree`)
Verified: 10 Sep 2026
Axioms: Classical.choiceQuot.soundpropext

Read back from the Lean

For every type F equipped with a commutative ring structure, an integral-domain structure (IsDomain F), and decidable equality, for every natural number n, for every multivariate polynomial p in n variables over F (i.e. p : MvPolynomial (Fin n) F) that is nonzero, and for every finite subset S of F with positive cardinality, if the total degree of p is strictly less than the cardinality of S, then there exists a point x : Fin n → F all of whose coordinates lie in S (membership in Fintype.piFinset (fun _ : Fin n => S), i.e. x i ∈ S for every i : Fin n) such that the evaluation of p at x is nonzero in F. Quantifier/hypothesis order, all explicit: F → [CommRing F] → [IsDomain F] → [DecidableEq F] → n → p → hypothesis hp : p ≠ 0 → S → hypothesis hS : 0 < S.card → hypothesis hd : p.totalDegree < S.card → conclusion ∃ x ∈ Fintype.piFinset (fun _ : Fin n => S), MvPolynomial.eval x p ≠ 0. The inequality p.totalDegree < S.card is strict. The conclusion is existential: at least one point of S^n gives a nonzero value (not that all or almost all do). The set S is not assumed to be finite-by-typeclass; it is an arbitrary Finset F, and the domain F is arbitrary (possibly infinite), restricted only by the ring/domain/decidability instances. The number of variables n is universally quantified and may be 0.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- Schwartz–Zippel, PIT form: a nonzero polynomial of total degree < |S| has a nonvanishing point in S^n. -/
theorem schwartz_zippel_exists_nonzero_eval {F : Type*} [CommRing F] [IsDomain F] [DecidableEq F]
    {n : ℕ} {p : MvPolynomial (Fin n) F} (hp : p ≠ 0) {S : Finset F} (hS : 0 < S.card)
    (hd : p.totalDegree < S.card) :
    ∃ x ∈ Fintype.piFinset (fun _ : Fin n => S), MvPolynomial.eval x p ≠ 0 := by
  by_contra h
  push Not at h
  have hcard : ((Fintype.piFinset (fun _ : Fin n => S)).filter
      (fun f => MvPolynomial.eval f p = 0)).card = S.card ^ n := by
    rw [Finset.filter_true_of_mem]
    · exact Fintype.card_piFinset_const S n
    · intro x hx; exact h x hx
  have hsz := MvPolynomial.schwartz_zippel_totalDegree (n := n) hp S
  rw [hcard] at hsz
  have hc : (0 : ℚ≥0) < S.card := by exact_mod_cast hS
  have hcpow : ((S.card : ℚ≥0)) ^ n ≠ 0 := pow_ne_zero _ hc.ne'
  have hle1 : (1 : ℚ≥0) ≤ (p.totalDegree : ℚ≥0) / S.card := by
    have h_eq : ((S.card ^ n : ℕ) : ℚ≥0) / ((S.card : ℚ≥0) ^ n) = 1 := by
      rw [Nat.cast_pow, div_self hcpow]
    rwa [h_eq] at hsz
  have hle2 : (S.card : ℚ≥0) ≤ (p.totalDegree : ℚ≥0) := by
    have hmul := mul_le_mul_of_nonneg_right hle1 (le_of_lt hc)
    rwa [one_mul, div_mul_cancel₀ _ hc.ne'] at hmul
  have hnat : S.card ≤ p.totalDegree := by exact_mod_cast hle2
  omega

Discuss this result Challenge it