English
For any family P_i and finite set s, the coefficient of ∑_{i∈s} deg_m(P_i) in the product ∏_{i∈s} P_i is equal to ∏_{i∈s} lc_m(P_i).
Русский
Для семейства P_i и конечного множества s коэффициент при сумме степеней в произведении ∏_{i∈s} P_i равен произведению lc_m(P_i).
LaTeX
$$$$ \operatorname{coeff}\left( \sum_{i\in s} \deg_m(P_i), \prod_{i\in s} P_i \right) = \prod_{i\in s} \operatorname{leadingCoeff}_m(P_i). $$$$
Lean4
theorem coeff_prod_sum_degree {ι : Type*} (P : ι → MvPolynomial σ R) (s : Finset ι) :
coeff (∑ i ∈ s, m.degree (P i)) (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i) := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert a s has hrec =>
simp only [Finset.prod_insert has, Finset.sum_insert has]
rw [coeff_mul_of_add_of_degree_le (le_of_eq rfl) degree_prod_le]
exact congr_arg₂ _ rfl hrec
