English
For a multiset s of scalars, the product ∏_{λ∈s} (X+λ) expands into coefficients given by esymm of s.
Русский
Для мультисета скаляров произведение ∏_{λ∈s} (X+λ) разворачивается в коэффициенты, заданные esymm s.
LaTeX
$$$$\\prod_{\\lambda \\in s} (X+\\lambda) = \\sum_{k\\ge 0} C_{k} X^{|s|-k},\\quad C_{k}=\\mathrm{esymm}_{|s|-k}(s).$$$$
Lean4
/-- A sum version of **Vieta's formula** for `Multiset`: the product of the linear terms `X + λ`
where `λ` runs through a multiset `s` is equal to a linear combination of the symmetric functions
`esymm s` of the `λ`'s . -/
theorem prod_X_add_C_eq_sum_esymm (s : Multiset R) :
(s.map fun r => X + C r).prod =
∑ j ∈ Finset.range (Multiset.card s + 1), (C (s.esymm j) * X ^ (Multiset.card s - j)) :=
by
classical
rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ← bind_powerset_len, map_bind, sum_bind,
Finset.sum_eq_multiset_sum, Finset.range_val, map_congr (Eq.refl _)]
intro _ _
rw [esymm, ← sum_hom', ← sum_map_mul_right, map_congr (Eq.refl _)]
intro s ht
rw [mem_powersetCard] at ht
dsimp
rw [prod_hom' s (Polynomial.C : R →+* R[X])]
simp [ht, prod_replicate, map_id', card_sub]
