The polynomial zero bound on the full affine parameter space, with its field-size saving retained in multiplicative form. This is the Schwartz–Zippel lemma MvPolynomial.schwartz_zippel_totalDegree_card applied to the whole finite field.

theorem CCDN.finite_field_polynomial_zeros_mul_card {K : Type u_1} {τ : Type u_2} [Field K] [Fintype K] [Fintype τ] (f : MvPolynomial τ K) (hf : f ≠ 0) : Nat.card { x : τ → K // (MvPolynomial.eval x) f = 0 } * Fintype.card K ≤ f.totalDegree * Fintype.card K ^ Fintype.card τ

Schwartz--Zippel for an arbitrary finite coordinate type.