English
In the multivariate Viète setting, for k ≤ card σ, the coefficient of X^k in ∏_{i∈σ} (X + C X_i) equals esymm(σ, card σ − k).
Русский
В многозначной версии формулы Виета для σ: коэффициент при X^k в ∏_{i∈σ} (X + C X_i) равен esymm(σ, card σ − k).
LaTeX
$$$$ \\Big( \\prod_{i\\in\\sigma} (X + C (MvPolynomial.X_i)) \\Big).coeff\\ k = MvPolynomial.esymm(\\sigma, R, \\lvert \\sigma\\rvert - k). $$$$
Lean4
theorem prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ) :
(∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i)) : Polynomial _).coeff k =
MvPolynomial.esymm σ R (card σ - k) :=
by
let s := Finset.univ.val.map fun i => (MvPolynomial.X i : MvPolynomial σ R)
have : Fintype.card σ = Multiset.card s := by rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
rw [this] at h ⊢
rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
convert Multiset.prod_X_add_C_coeff s h
dsimp
simp_rw [s, Multiset.map_map, Function.comp_apply]
