English
For s a multiset and k in N with k ≤ |s|, the k-th coefficient of ∏_{i∈s} (X+ C r_i) equals esymm(|s|-k) of r_i.
Русский
Для мультисета s и k≤|s|, коэффициент k слева равен esymm(|s|-k) последовательности r_i.
LaTeX
$$$$\\left[\\prod_{i\\in s} (X + r_i)\\right]_{X^k} = \\mathrm{esymm}_{|s|-k}(r_i)$$$$
Lean4
/-- Vieta's formula for the coefficients of the product of linear terms `X + λ` where `λ` runs
through a multiset `s` : the `k`th coefficient is the symmetric function `esymm (card s - k) s`. -/
theorem prod_X_add_C_coeff (s : Multiset R) {k : ℕ} (h : k ≤ Multiset.card s) :
(s.map fun r => X + C r).prod.coeff k = s.esymm (Multiset.card s - k) :=
by
convert Polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k using 1
simp_rw [finset_sum_coeff, coeff_C_mul_X_pow]
rw [Finset.sum_eq_single_of_mem (Multiset.card s - k) _] <;> grind
