Theorems · Theorem · commutative algebra

MvPolynomial.prod_C_add_X_eq_sum_esymm

∀ (R : Type u_1) (σ : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype σ],
  ∏ i, (Polynomial.X + Polynomial.C (MvPolynomial.X i)) =
    ∑ j ∈ Finset.range (Fintype.card σ + 1),
      Polynomial.C (MvPolynomial.esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

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.

Defined in

Mathlib.RingTheory.Polynomial.Vieta

Cited by

0 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFintype