schwartz_zippel_zero_count_le

theoremverified

Let F be an integral domain, S a nonempty finite subset of F, n a positive integer, and p a nonzero polynomial in n variables over F of total degree d. Then the number of points x of S^n at which p vanishes is at most d·|S|^(n−1); equivalently, the fraction of the points of S^n at which p vanishes is at most d/|S|.

Statement

open scoped Finset in
theorem schwartz_zippel_zero_count_le {F : Type*} [CommRing F] [IsDomain F] [DecidableEq F]
    {n : ℕ} (hn : 0 < n) {p : MvPolynomial (Fin n) F} (hp : p ≠ 0) {S : Finset F}
    (hS : 0 < S.card) :
    #{x ∈ Fintype.piFinset (fun _ : Fin n => S) | MvPolynomial.eval x p = 0}
      ≤ p.totalDegree * S.card ^ (n - 1)

Source: Schwartz 1980; Zippel 1979 — counting form of the Schwartz–Zippel lemma (Motwani & Raghavan, Randomized Algorithms, ch. 7); derived here from Mathlib `Mathlib.Algebra.MvPolynomial.SchwartzZippel`, `MvPolynomial.schwartz_zippel_totalDegree`.
Verified: 11 Sep 2026
Axioms: Classical.choiceQuot.soundpropext

Read back from the Lean

Let F be a commutative ring (CommRing F) that is an integral domain (IsDomain F: nontrivial and with no zero divisors) with decidable equality, let n be a natural number with 0 < n, let p be a multivariate polynomial in n variables over F (p : MvPolynomial (Fin n) F), assume p ≠ 0, and let S be a finite set of elements of F with 0 < S.card (i.e. S is nonempty). Then the number of n-tuples x = (x_0, …, x_{n-1}) with every coordinate x_i ∈ S (i.e. points of the grid S^n, encoded as the dependent function space Fin n → F, restricted to functions taking values in S) at which p vanishes (MvPolynomial.eval x p = 0) is at most totalDegree(p) · S.card^(n-1), where totalDegree(p) is the total degree of p and the inequality is non-strict. Concretely: the cardinality of the finset of x in Fintype.piFinset (fun _ : Fin n => S) satisfying MvPolynomial.eval x p = 0 is ≤ p.totalDegree * S.card ^ (n - 1). This is the Schwartz–Zippel style bound on the number of zeros of a nonzero polynomial over an integral domain, counted over the grid S^n.

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

open scoped Finset in
/-- Counting form of the Schwartz–Zippel lemma: a nonzero polynomial of total degree d vanishes on at most d·|S|^(n−1) points of S^n. -/
theorem schwartz_zippel_zero_count_le {F : Type*} [CommRing F] [IsDomain F] [DecidableEq F]
    {n : ℕ} (hn : 0 < n) {p : MvPolynomial (Fin n) F} (hp : p ≠ 0) {S : Finset F}
    (hS : 0 < S.card) :
    #{x ∈ Fintype.piFinset (fun _ : Fin n => S) | MvPolynomial.eval x p = 0}
      ≤ p.totalDegree * S.card ^ (n - 1) := by
  have hsz := MvPolynomial.schwartz_zippel_totalDegree (n := n) hp S
  have hcpos : (0 : ℚ≥0) < (S.card : ℚ≥0) := by exact_mod_cast hS
  have hcne : (S.card : ℚ≥0) ≠ 0 := hcpos.ne'
  have hcpowpos : (0 : ℚ≥0) < (S.card : ℚ≥0) ^ n := pow_pos hcpos n
  have hcpowne : (S.card : ℚ≥0) ^ n ≠ 0 := hcpowpos.ne'
  have hmul := mul_le_mul_of_nonneg_right hsz (le_of_lt hcpowpos)
  rw [div_mul_cancel₀ _ hcpowne] at hmul
  have hpow : (↑S.card : ℚ≥0) ^ n = (↑S.card : ℚ≥0) ^ (n - 1) * ↑S.card := by
    conv_lhs => rw [← Nat.sub_add_cancel hn]
    rw [pow_succ]
  have hrewrite : (↑p.totalDegree / (↑S.card : ℚ≥0)) * (↑S.card : ℚ≥0) ^ n
      = (↑(p.totalDegree * S.card ^ (n - 1)) : ℚ≥0) := by
    rw [Nat.cast_mul, Nat.cast_pow, hpow,
        mul_comm ((↑S.card : ℚ≥0) ^ (n - 1)) (↑S.card), ← mul_assoc,
        div_mul_cancel₀ _ hcne]
  rw [hrewrite] at hmul
  exact_mod_cast hmul

Discuss this result Challenge it