A nonzero polynomial over a characteristic-zero domain has a nonzero value at an integer point with every coordinate between 0 and its degree. This is the combinatorial Nullstellensatz MvPolynomial.eq_zero_of_eval_zero_at_prod_finset on the grid {0,...,D}.

theorem CCDN.exists_integer_grid_eval_ne_zero_of_degreeOf {R : Type u_1} {σ : Type u_2} [CommRing R] [IsDomain R] [CharZero R] [Finite σ] (f : MvPolynomial σ R) (hf : f ≠ 0) (D : ℕ) (hdeg : ∀ (i : σ), MvPolynomial.degreeOf i f ≤ D) : ∃ (v : σ → ℤ), (∀ (i : σ), 0 ≤ v i ∧ v i ≤ ↑D) ∧ (MvPolynomial.eval fun (i : σ) => ↑(v i)) f ≠ 0

A nonzero polynomial with coordinate degrees at most D has a nonzero value on the integer grid {0,...,D}, in any finite number of variables. Unlike the total-degree version, the side length does not grow with the number of variables.

theorem CCDN.exists_integer_grid_eval_ne_zero_of_totalDegree {R : Type u_1} {σ : Type u_2} [CommRing R] [IsDomain R] [CharZero R] [Finite σ] (f : MvPolynomial σ R) (hf : f ≠ 0) (A : ℕ) (hd : f.totalDegree ≤ A) : ∃ (v : σ → ℤ), (∀ (i : σ), 0 ≤ v i ∧ v i ≤ ↑A) ∧ (MvPolynomial.eval fun (i : σ) => ↑(v i)) f ≠ 0

A nonzero polynomial of total degree at most A over a characteristic-zero domain has a nonzero value on the integer grid {0,...,A}.

theorem CCDN.exists_integer_grid_eval_ne_zero {σ : Type u_1} [Finite σ] (f : MvPolynomial σ ℤ) (hf : f ≠ 0) (A : ℕ) (hd : f.totalDegree ≤ A) : ∃ (v : σ → ℤ), (∀ (i : σ), 0 ≤ v i ∧ v i ≤ ↑A) ∧ (MvPolynomial.eval v) f ≠ 0

The integer case of exists_integer_grid_eval_ne_zero_of_totalDegree. The bound is independent of the number and names of the coordinates.