Theorems · Theorem · commutative algebra

Multiset.prod_X_add_C_coeff

∀ {R : Type u_1} [inst : CommSemiring R] (s : Multiset R) {k : ℕ},
  k ≤ s.card → (Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod.coeff k = s.esymm (s.card - k)

Vieta's formula for the coefficients of the product of linear terms X + λ where λ runs through a multiset s : the kth coefficient is the symmetric function esymm (card s - k) s.

Defined in

Mathlib.RingTheory.Polynomial.Vieta

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiring