English
If q is homogeneous of degree n, and hpq: MvPolynomial.aeval (![X,1]) q = p, then p.homogenize n = q.
Русский
Если q гомогенный степени n и hpq: aeval ![X,1] q = p, то p.homogenize n = q.
LaTeX
$$$\\text{If } q \\text{ is homogeneous of degree } n \\text{ and } aeval \\!([X,1]) q = p, \\text{ then } p.homogenize\\ n = q.$$$
Lean4
theorem eval_homogenize {p : K[X]} {n : ℕ} (hn : p.natDegree ≤ n) (x : Fin 2 → K) (hx : x 1 ≠ 0) :
MvPolynomial.eval x (p.homogenize n) = p.eval (x 0 / x 1) * x 1 ^ n :=
by
simp only [homogenize, Polynomial.eval_eq_sum_range' (Nat.lt_succ.mpr hn),
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Finset.sum_mul, MvPolynomial.eval_sum]
refine Finset.sum_congr rfl fun k hk ↦ ?_
rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index', Finsupp.prod_single_index,
Finsupp.prod_single_index, pow_sub₀]
· ring
all_goals simp_all [pow_add, Nat.lt_add_one_iff]
