Chapter 35, Lemma 1: polynomial zeros

Proved

BookSixth.polynomial_zero_bound

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

Over a finite field of size q, a nonzero polynomial in a positive number n of variables has at most d q^(n−1) zeros, where d is its total degree.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.polynomial_zero_bound {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (hn : 0 < n) (p : MvPolynomial (Fin n) F) (hp : p ≠ 0) :
    (Finset.univ.filter (fun x : Fin n → F => MvPolynomial.eval x p = 0)).card ≤
      p.totalDegree * Fintype.card F ^ (n-1) := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 35, Lemma 1: polynomial zeros, p. 249. https://doi.org/10.1007/978-3-662-57265-8_35

View graph