A prime scaling preserves primitive integer equations when it does not divide the constant coefficient. This is the arithmetic input for affine scaling.

theorem CCDN.PrimitiveIntegerPolynomial.scaledHomogenize {n : ℕ} {f : MvPolynomial (Fin n) ℤ} (hf : PrimitiveIntegerPolynomial f) (d : ℕ) {p : ℕ} (hp : Nat.Prime p) (hp0 : ¬↑p ∣ f.coeff 0) : PrimitiveIntegerPolynomial (CCDN.scaledHomogenize d (↑p) f)

If f is a primitive integer polynomial and the prime p does not divide its constant coefficient, then the scaled homogenization scaledHomogenize d p f is primitive.