English
A finite product of polynomials, each homogeneous of degree n_i, is homogeneous of degree sum n_i.
Русский
Конечный произведение полиномов, каждый из которых однороден степени n_i, однородно степени суммы n_i.
LaTeX
$$For Finite set s, φ_i with n_i, if ∀ i ∈ s, IsHomogeneous(φ_i, n_i), then IsHomogeneous(∏ i ∈ s, φ_i, ∑ i ∈ s, n_i).$$
Lean4
theorem prod {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : ι → ℕ)
(h : ∀ i ∈ s, IsHomogeneous (φ i) (n i)) : IsHomogeneous (∏ i ∈ s, φ i) (∑ i ∈ s, n i) := by
classical
revert h
refine Finset.induction_on s ?_ ?_
· intro
simp only [isHomogeneous_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 (by grind)).mul (IH _)
grind
