Chapter 35, Lemma 2: vanishing polynomial

Proved

BookSixth.vanishing_polynomial

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

proofs-from-the-booksixth-edition

If fewer than binomial(n+d,d) points are prescribed in finite affine n-space, a nonzero polynomial of total degree at most d vanishes on all of them.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.vanishing_polynomial {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} (E : Finset (Fin n → F)) (hE : E.card < Nat.choose (n+d) d) :
    ∃ p : MvPolynomial (Fin n) F, p ≠ 0 ∧ p.totalDegree ≤ d ∧
      ∀ x ∈ E, MvPolynomial.eval x p = 0 := by sorry

Source

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

View graph