English
A multivariate Viète-type identity: viewing X_i as variables, the product over i in σ of (X + C X_i) equals a linear combination ∑_{j=0}^{|σ|} C(esymm(σ) j) X^{|σ|−j} in which esymm denotes elementary symmetric sums of the variables X_i.
Русский
Обобщение формулы Виета для многофункций: если рассматривать X_i как переменные, то произведение по i∈σ (X + C X_i) равно линейной комбинации ∑_{j=0}^{|σ|} C(esymm(σ) j) X^{|σ|−j}, где esymm — элементарные симметрические суммы переменных X_i.
LaTeX
$$$$ \\prod_{i\\in\\sigma} (X + C (M vPolynomial.X_i)) = \\sum_{j=0}^{|\\sigma|} C\\big(MvPolynomial.esymm \\sigma R j\\big) X^{|\\sigma| - j}. $$$$
Lean4
/-- A sum version of Vieta's formula for `MvPolynomial`: viewing `X i` as variables,
the product of linear terms `λ + X i` is equal to a linear combination of
the symmetric polynomials `esymm σ R j`. -/
theorem prod_C_add_X_eq_sum_esymm :
(∏ i : σ, (Polynomial.X + Polynomial.C (MvPolynomial.X i))) =
∑ j ∈ range (card σ + 1), Polynomial.C (MvPolynomial.esymm σ R j) * Polynomial.X ^ (card σ - j) :=
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]
simp_rw [this, MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]
convert Multiset.prod_X_add_C_eq_sum_esymm s
simp_rw [s, Multiset.map_map, Function.comp_apply]
