English
A product over a finite index set of weighted homogeneous polynomials is weighted homogeneous with degree equal to the sum of the degrees.
Русский
Произведение по конечному индексу взвешенно однородных полиномов имеет сумму степеней как степень.
LaTeX
$$∏ φ_i is weighted homogeneous of degree sum n_i$$
Lean4
/-- A product of weighted homogeneous polynomials is weighted homogeneous, with weighted degree
equal to the sum of the weighted degrees. -/
theorem prod {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ι → M) {w : σ → M} :
(∀ i ∈ s, IsWeightedHomogeneous w (φ i) (n i)) → IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i) := by
classical
refine Finset.induction_on s ?_ ?_
· intro
simp only [isWeightedHomogeneous_one, Finset.sum_empty, Finset.prod_empty]
· intro i s his IH h
simp only [his, Finset.prod_insert, Finset.sum_insert, not_false_iff]
apply (h i (Finset.mem_insert_self _ _)).mul (IH _)
intro j hjs
exact h j (Finset.mem_insert_of_mem hjs)
