Primitive models preserve the equation's degree and homogeneous grading, and integer content removal does not increase coefficient height.

theorem CCDN.integer_scalar_factor_degree {σ : Type u_1} {f g : MvPolynomial σ ℤ} {c : ℤ} (hf : f ≠ 0) (hc : c ≠ 0) (he : f = MvPolynomial.C c * g) : g.totalDegree = f.totalDegree

If a nonzero integer polynomial factors as f = C c * g with c ≠ 0, then g has the same total degree as f.

theorem CCDN.integer_scalar_factor_coefficient_bound {σ : Type u_1} {f g : MvPolynomial σ ℤ} {c : ℤ} (hc : c ≠ 0) (he : f = MvPolynomial.C c * g) (m : σ →₀ ℕ) : |↑(g.coeff m)| ≤ |↑(f.coeff m)|

If f = C c * g with a nonzero integer c, then every coefficient of g is at most the corresponding coefficient of f in absolute value.

theorem CCDN.exists_primitive_integer_model {σ : Type u_1} (f : MvPolynomial σ ℚ) (hf : f ≠ 0) : ∃ (g : MvPolynomial σ ℤ) (a : ℚ), PrimitiveIntegerPolynomial g ∧ a ≠ 0 ∧ (MvPolynomial.map (Int.castRingHom ℚ)) g = MvPolynomial.C a * f

Every nonzero rational multivariate polynomial has a primitive integer model differing by a nonzero rational scalar.

theorem CCDN.rational_scalar_model_degree {σ : Type u_1} {f : MvPolynomial σ ℚ} {g : MvPolynomial σ ℤ} {a : ℚ} (ha : a ≠ 0) (hf : f ≠ 0) (he : (MvPolynomial.map (Int.castRingHom ℚ)) g = MvPolynomial.C a * f) : g.totalDegree = f.totalDegree

An integer polynomial g whose image over ℚ is a nonzero rational multiple C a * f of a nonzero polynomial f has the same total degree as f.

theorem CCDN.rational_scalar_model_homogeneous {σ : Type u_1} {f : MvPolynomial σ ℚ} {g : MvPolynomial σ ℤ} {a : ℚ} {d : ℕ} (he : (MvPolynomial.map (Int.castRingHom ℚ)) g = MvPolynomial.C a * f) (hf : f.IsHomogeneous d) : g.IsHomogeneous d

If the image over ℚ of an integer polynomial g is C a * f for a homogeneous polynomial f of degree d, then g is homogeneous of degree d.

theorem CCDN.rational_scalar_model_zero_iff {σ : Type u_1} {f : MvPolynomial σ ℚ} {g : MvPolynomial σ ℤ} {a : ℚ} (ha : a ≠ 0) (he : (MvPolynomial.map (Int.castRingHom ℚ)) g = MvPolynomial.C a * f) (x : σ → ℚ) : (MvPolynomial.eval x) ((MvPolynomial.map (Int.castRingHom ℚ)) g) = 0 ↔ (MvPolynomial.eval x) f = 0

If the image over ℚ of an integer polynomial g is C a * f with a ≠ 0, then g and f have the same rational zeros.