mathlib

05d8b4f3 - feat(ring_theory/polynomial/vieta): add version of prod_X_add_C_eq_sum_esymm for multiset (#15008)

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`: ```lean 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 ```lean 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`: ```lean 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 ```lean 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](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20fintype.20enumerating.20a.20multiset) 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