English
Let ι be a type, s a finite set of ι, p: ι → R[X], n: ι → ℕ. If for all i ∈ s we have natDegree(p i) ≤ n i, then homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i) = ∏ i ∈ s, homogenize (p i) (n i).
Русский
Пусть ι — множество, s — конечное подмножество; p : ι → R[X], n : ι → ℕ. Если для всех i ∈ s natDegree(p i) ≤ n i, то гомогенизация произведения равна произведению гомогенизаций:
LaTeX
$$$\\operatorname{homogenize}\\left(\\prod_{i\\in s} p_i,\\sum_{i\\in s} n_i\\right) = \\prod_{i\\in s} \\operatorname{homogenize}(p_i, n_i).$$$
Lean4
theorem homogenize_finsetProd {ι : Type*} {s : Finset ι} {p : ι → R[X]} {n : ι → ℕ}
(h : ∀ i ∈ s, (p i).natDegree ≤ n i) : homogenize (∏ i ∈ s, p i) (∑ i ∈ s, n i) = ∏ i ∈ s, homogenize (p i) (n i) :=
by
induction s using Finset.cons_induction with
| empty => simp
| cons i s hi ihs =>
simp only [prod_cons, sum_cons, forall_mem_cons] at *
rw [homogenize_mul _ _ h.1, ihs h.2]
exact (natDegree_prod_le _ _).trans (sum_le_sum h.2)
