Commit 2022-08-16 04:10 05d8b4f3

feat(ring_theory/polynomial/vieta): add version of prod_X_add_C_eq_sum_esymm for multiset (#15008) This is a proof of Vieta's formula for multiset:

lemma multiset.prod_X_add_C_eq_sum_esymm (s : multiset R) :
  (s.map (λ r, polynomial.X  + polynomial.C r)).prod 
 = ∑ j in finset.range (s.card + 1), (polynomial.C (s.esymm j) * polynomial.X ^ (s.card - j))

where

def multiset.esymm (s : multiset R) (n : ℕ) : R := ((s.powerset_len n).map multiset.prod).sum

From this, we deduce the proof of the formula for mv_polynomial:

lemma prod_C_add_X_eq_sum_esymm :
  (∏ i : σ, (polynomial.X + polynomial.C (X i)) : polynomial (mv_polynomial σ R) )=
  ∑ j in range (card σ + 1),  (polynomial.C (esymm σ R j) * polynomial.X ^ (card σ - j))

with

def mv_polynomial.esymm (n : ℕ) : mv_polynomial σ R := ∑ t in powerset_len n univ, ∏ i in t, X i

It is better to go in this direction since there does not seem to be a natural way to prove the multiset version from the mv_polynomial version due to the difficulty to enumerate the elements of a multiset with a fintype, see this Zulip thread and the discussion from https://github.com/leanprover-community/mathlib/pull/14908. We prove, as suggested in [#14908](https://github.com/leanprover-community/mathlib/pull/14908#discussion_r905667015) , that mv_polynomial.esymm is obtained by specialising multiset.esymm. However, we do not refactor the results of ring_theory/polynomial/symmetric in terms of multiset.esymm. From flt-regular