Integral scaled homogenization. The point (h,x) on the homogeneous model corresponds to the original integer affine point x, without dividing coordinates.

theorem CCDN.homogenizedExponent_value {R : Type u_1} [CommRing R] {n : ℕ} (d : ℕ) (h : R) (x : Fin n → R) (m : Fin n →₀ ℕ) : ((homogenizedExponent d m).prod fun (j : Fin (n + 1)) (e : ℕ) => Fin.cons h x j ^ e) = h ^ (d - m.sum fun (x : Fin n) (e : ℕ) => e) * m.prod fun (j : Fin n) (e : ℕ) => x j ^ e

The monomial with exponent homogenizedExponent d m evaluated at (h, x) equals h ^ (d - |m|) times the monomial x ^ m.

theorem CCDN.scaledHomogenize_eval {R : Type u_1} [CommRing R] {n d : ℕ} (h : R) (f : MvPolynomial (Fin n) R) (hf : f.totalDegree ≤ d) (x : Fin n → R) : (MvPolynomial.eval (Fin.cons h x)) (scaledHomogenize d h f) = h ^ d * (MvPolynomial.eval x) f

If f has total degree at most d, then evaluating scaledHomogenize d h f at the point (h, x) gives h ^ d times the value of f at x.

theorem CCDN.scaledHomogenize_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} (d : ℕ) {h : R} (hh : h ≠ 0) {f : MvPolynomial (Fin n) R} (hf : f ≠ 0) : scaledHomogenize d h f ≠ 0

Over a domain, the scaled homogenization of a nonzero polynomial with a nonzero scaling factor h is nonzero.

theorem CCDN.scaledHomogenize_integer_coefficient_lower {n : ℕ} (d : ℕ) {h : ℤ} (hh : 1 ≤ h) (f : MvPolynomial (Fin n) ℤ) (m : Fin n →₀ ℕ) : |↑(f.coeff m)| ≤ |↑((scaledHomogenize d h f).coeff (homogenizedExponent d m))|

A scaling factor at least one does not decrease any original coefficient.

theorem CCDN.exists_scaledHomogenize_top_coefficient {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (hf : f ≠ 0) {h : ℤ} (hh : 1 ≤ h) : ∃ (m : Fin n →₀ ℕ), (m.sum fun (x : Fin n) (e : ℕ) => e) = f.totalDegree ∧ ↑h ^ f.totalDegree ≤ |↑((scaledHomogenize f.totalDegree h f).coeff (homogenizedExponent f.totalDegree m))|

A highest-degree nonzero coefficient gains the full factor h^d.