The Schwartz–Zippel lemma over an arbitrary finite type of variables

Mathlib's MvPolynomial.schwartz_zippel_totalDegree is stated for variables indexed by Fin n, as an inequality between nonnegative rationals. This file transports it to an arbitrary finite type of variables and clears the denominators, giving an inequality between natural numbers.

Main results

• MvPolynomial.schwartz_zippel_totalDegree_card: a nonzero polynomial p in the variables σ has at most p.totalDegree * #S ^ (card σ - 1) zeros in S ^ σ, stated multiplicatively.

theorem MvPolynomial.schwartz_zippel_totalDegree_card {R : Type u_1} {σ : Type u_2} [CommRing R] [IsDomain R] [DecidableEq R] [Fintype σ] [DecidableEq σ] {p : MvPolynomial σ R} (hp : p ≠ 0) (S : Finset R) : {x ∈ Fintype.piFinset fun (x : σ) => S | (eval x) p = 0}.card * S.card ≤ p.totalDegree * S.card ^ Fintype.card σ

The Schwartz–Zippel lemma for an arbitrary finite type of variables, with natural-number cardinalities: a nonzero polynomial p vanishes at no more than a proportion p.totalDegree / #S of the points of S ^ σ.