Translation preserves the leading homogeneous equation exactly. Bounded integer translations make the constant coefficient nonzero in every dimension.

theorem CCDN.affineTranslation_leading_homogeneousComponent {R : Type u_1} [CommRing R] [Nontrivial R] {n : ℕ} (a : Fin n → R) (f : MvPolynomial (Fin n) R) : (MvPolynomial.homogeneousComponent ((affineTranslation R a) f).totalDegree) ((affineTranslation R a) f) = (MvPolynomial.homogeneousComponent f.totalDegree) f

Affine translation of the variables does not change the leading form: the top-degree homogeneous component of affineTranslation R a f equals that of f.

theorem CCDN.exists_bounded_affine_translation_nonzero_constant {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf : f ≠ 0) : ∃ (a : Fin n → ℤ), (∀ (j : Fin n), 0 ≤ a j ∧ a j ≤ ↑f.totalDegree) ∧ ((affineTranslation ℤ a) f).coeff 0 ≠ 0

A nonzero integral polynomial f in n variables has an integral translate with nonzero constant coefficient by a vector whose entries lie in [0, deg f].