feat(ring_theory/polynomial/vieta): add version of prod_X_add_C_eq_su…

…m_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 #14908.

We prove, as suggested in [#14908](#14908 (comment)) , 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

src/ring_theory/polynomial/symmetric.lean

@@ -44,6 +44,15 @@ open equiv (perm)
 open_locale big_operators
 noncomputable theory
 
+namespace multiset
+
+variables {R : Type*} [comm_semiring R]
+
+/-- The `n`th elementary symmetric function evaluated at the elements of `s` -/
+def esymm (s : multiset R) (n : ℕ) : R := ((s.powerset_len n).map multiset.prod).sum
+
+end multiset
+
 namespace mv_polynomial
 
 variables {σ : Type*} {R : Type*}
@@ -121,6 +130,17 @@ variables (σ R) [comm_semiring R] [comm_semiring S] [fintype σ] [fintype τ]
 def esymm (n : ℕ) : mv_polynomial σ R :=
 ∑ t in powerset_len n univ, ∏ i in t, X i
 
+/-- The `n`th elementary symmetric `mv_polynomial σ R` is obtained by evaluating the
+`n`th elementary symmetric at the `multiset` of the monomials -/
+lemma esymm_eq_multiset.esymm (n : ℕ) :
+  esymm σ R n =
+  multiset.esymm (multiset.map (λ i : σ, (X i : mv_polynomial σ R)) finset.univ.val) n :=
+begin
+  rw [esymm, multiset.esymm, finset.sum_eq_multiset_sum],
+  conv_lhs { congr, congr, funext, rw finset.prod_eq_multiset_prod },
+  rw [multiset.powerset_len_map, ←map_val_val_powerset_len, multiset.map_map, multiset.map_map],
+end
+
 /-- We can define `esymm σ R n` by summing over a subtype instead of over `powerset_len`. -/
 lemma esymm_eq_sum_subtype (n : ℕ) : esymm σ R n =
   ∑ t : {s : finset σ // s.card = n}, ∏ i in (t : finset σ), X i :=

src/ring_theory/polynomial/vieta.lean

@@ -9,95 +9,137 @@ import ring_theory.polynomial.symmetric
 /-!
 # Vieta's Formula
 
-The main result is `vieta.prod_X_add_C_eq_sum_esymm`, which shows that the product of linear terms
-`λ + X i` is equal to a linear combination of the symmetric polynomials `esymm σ R j`.
+The main result is `multiset.prod_X_add_C_eq_sum_esymm`, which shows that the product of
+linear terms ` X + λ` with `λ` in a `multiset s` is equal to a linear combination of the
+symmetric functions `esymm s`.
 
-## Implementation Notes:
-
-We first take the viewpoint where the "roots" `X i` are variables. This means we work over
-`polynomial (mv_polynomial σ R)`, which enables us to talk about linear combinations of
-`esymm σ R j`. We then derive Vieta's formula in `polynomial R` by giving a
-valuation from each `X i` to `r i`.
+From this, we deduce `mv_polynomial.prod_X_add_C_eq_sum_esymm` which is the equivalent formula
+for the product of linear terms `X + X i` with `i` in a `fintype σ` as a linear combination
+of the symmetric polynomials `esymm σ R j`.
 
 -/
 
 open_locale big_operators polynomial
 
-open finset polynomial fintype
+namespace multiset
 
-namespace mv_polynomial
+section semiring
 
 variables {R : Type*} [comm_semiring R]
-variables (σ : Type*) [fintype σ]
 
-/-- A sum version of Vieta's formula. 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`. -/
-lemma prod_X_add_C_eq_sum_esymm :
-  (∏ i : σ, (polynomial.C (X i) + polynomial.X) : polynomial (mv_polynomial σ R) )=
-  ∑ j in range (card σ + 1),
-    (polynomial.C (esymm σ R j) * polynomial.X ^ (card σ - j)) :=
+/-- A sum version of Vieta's formula for `multiset`: the product of the linear terms `X + λ` where
+`λ` runs through a multiset `s` is equal to a linear combination of the symmetric functions
+`esymm s` of the `λ`'s .-/
+lemma 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)) :=
 begin
   classical,
-  rw [prod_add, sum_powerset],
-  refine sum_congr begin congr end (λ j hj, _),
-  rw [esymm, map_sum, sum_mul],
-  refine sum_congr rfl (λ t ht, _),
-  have h : (univ \ t).card = card σ - j :=
-  by { rw card_sdiff (mem_powerset_len.mp ht).1, congr, exact (mem_powerset_len.mp ht).2 },
-  rw [map_prod, prod_const, ← h],
+  rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ←bind_powerset_len, function.comp,
+    map_bind, sum_bind, finset.sum_eq_multiset_sum, finset.range_coe, map_congr (eq.refl _)],
+  intros _ _,
+  rw [esymm, ←sum_hom', ←sum_map_mul_right, map_congr (eq.refl _)],
+  intros _ ht,
+  rw mem_powerset_len at ht,
+  simp [ht, map_const, prod_repeat, prod_hom', map_id', card_sub],
 end
 
-/-- A fully expanded sum version of Vieta's formula, evaluated at the roots.
-The product of linear terms `X + r i` is equal to `∑ j in range (n + 1), e_j * X ^ (n - j)`,
-where `e_j` is the `j`th symmetric polynomial of the constant terms `r i`. -/
-lemma prod_X_add_C_eval (r : σ → R) : ∏ i : σ, (polynomial.C (r i) + polynomial.X) =
-  ∑ i in range (card σ + 1), (∑ t in powerset_len i (univ : finset σ),
-    ∏ i in t, polynomial.C (r i)) * polynomial.X ^ (card σ - i) :=
+/-- Vieta's formula for the coefficients of the product of linear terms `X + λ` where `λ` runs
+through a multiset `s` : the `k`th coefficient is the symmetric function `esymm (card s - k) s`. -/
+lemma prod_X_add_C_coeff (s : multiset R) {k : ℕ} (h : k ≤ s.card):
+  polynomial.coeff (s.map (λ r, polynomial.X + polynomial.C r)).prod k =
+  s.esymm (s.card - k) :=
 begin
-  classical,
-  have h := @prod_X_add_C_eq_sum_esymm _ _ σ _,
-  apply_fun (polynomial.map (eval r)) at h,
-  rw [polynomial.map_prod, polynomial.map_sum] at h,
-  convert h,
-  simp only [eval_X, polynomial.map_add, polynomial.map_C, polynomial.map_X, eq_self_iff_true],
-  funext,
-  simp only [function.funext_iff, esymm, polynomial.map_C, polynomial.map_sum, map_sum,
-    polynomial.map_C, polynomial.map_pow, polynomial.map_X, polynomial.map_mul],
-  congr,
-  funext,
-  simp only [eval_prod, eval_X, map_prod],
+  convert polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k,
+  simp_rw [polynomial.finset_sum_coeff, polynomial.coeff_C_mul_X_pow],
+  rw finset.sum_eq_single_of_mem (s.card - k) _,
+  { rw if_pos (nat.sub_sub_self h).symm, },
+  { intros j hj1 hj2,
+    suffices : k ≠ card s - j,
+    { rw if_neg this, },
+    { intro hn,
+      rw [hn, nat.sub_sub_self (nat.lt_succ_iff.mp (finset.mem_range.mp hj1))] at hj2,
+      exact ne.irrefl hj2, }},
+  { rw finset.mem_range,
+    exact nat.sub_lt_succ s.card k }
+end
+
+end semiring
+
+section ring
+
+variables  {R : Type*} [comm_ring R]
+
+lemma esymm_neg (s : multiset R) (k : ℕ) :
+  (map has_neg.neg s).esymm k = (-1)^k * esymm s k :=
+begin
+  rw [esymm, esymm, ←multiset.sum_map_mul_left, multiset.powerset_len_map, multiset.map_map,
+    map_congr (eq.refl _)],
+  intros x hx,
+  rw [(by { exact (mem_powerset_len.mp hx).right.symm }), ←prod_repeat, ←multiset.map_const],
+  nth_rewrite 2 ←map_id' x,
+  rw [←prod_map_mul, map_congr (eq.refl _)],
+  exact λ z _, neg_one_mul z,
+end
+
+lemma prod_X_sub_C_eq_sum_esymm (s : multiset R) :
+  (s.map (λ t, polynomial.X - polynomial.C t)).prod =
+  ∑ j in finset.range (s.card + 1),
+  (-1)^j* (polynomial.C (s.esymm j) * polynomial.X ^ (s.card - j)) :=
+begin
+  conv_lhs { congr, congr, funext, rw sub_eq_add_neg, rw ←map_neg polynomial.C _, },
+  convert prod_X_add_C_eq_sum_esymm (map (λ t, -t) s) using 1,
+  { rwa map_map, },
+  { simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one], },
 end
 
-lemma esymm_to_sum (r : σ → R) (j : ℕ) : polynomial.C (eval r (esymm σ R j)) =
-  ∑ t in powerset_len j (univ : finset σ), ∏ i in t, polynomial.C (r i) :=
-by simp only [esymm, eval_sum, eval_prod, eval_X, map_sum, map_prod]
+lemma prod_X_sub_C_coeff (s : multiset R) {k : ℕ} (h : k ≤ s.card):
+  polynomial.coeff (s.map (λ t, polynomial.X - polynomial.C t)).prod k =
+  (-1)^(s.card - k) * s.esymm (s.card - k) :=
+begin
+  conv_lhs { congr, congr, congr, funext, rw sub_eq_add_neg, rw ←map_neg polynomial.C _, },
+  convert prod_X_add_C_coeff (map (λ t, -t) s) _ using 1,
+  { rwa map_map, },
+  { rwa [esymm_neg, card_map] },
+  { rwa card_map },
+end
+
+end ring
+
+end multiset
+
+namespace mv_polynomial
+
+open finset polynomial fintype
+
+variables (R σ : Type*) [comm_semiring R] [fintype σ]
+
+/-- A sum version of Vieta's formula for `mv_polynomial`: 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`. -/
+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)) :=
+begin
+  let s := (multiset.map (λ i : σ, (X i : mv_polynomial σ R)) finset.univ.val),
+  rw (_ : card σ = s.card),
+  { simp_rw [esymm_eq_multiset.esymm σ R _, finset.prod_eq_multiset_prod],
+    convert multiset.prod_X_add_C_eq_sum_esymm s,
+    rwa multiset.map_map, },
+  { rw multiset.card_map, exact rfl, }
+end
 
-/-- Vieta's formula for the coefficients of the product of linear terms `X + r i`,
-The `k`th coefficient is `∑ t in powerset_len (card σ - k) (univ : finset σ), ∏ i in t, r i`,
-i.e. the symmetric polynomial `esymm σ R (card σ - k)` of the constant terms `r i`. -/
-lemma prod_X_add_C_coeff (r : σ → R) (k : ℕ) (h : k ≤ card σ):
-  polynomial.coeff (∏ i : σ, (polynomial.C (r i) + polynomial.X)) k =
-  ∑ t in powerset_len (card σ - k) (univ : finset σ), ∏ i in t, r i :=
+lemma prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ):
+  (∏ i : σ, (polynomial.X + polynomial.C (X i)) : polynomial (mv_polynomial σ R) ).coeff k =
+  esymm σ R (card σ - k) :=
 begin
-  have hk : filter (λ (x : ℕ), k = card σ - x) (range (card σ + 1)) = {card σ - k} :=
-  begin
-    refine finset.ext (λ a, ⟨λ ha, _, λ ha, _ ⟩),
-    rw mem_singleton,
-    have hσ := (tsub_eq_iff_eq_add_of_le (mem_range_succ_iff.mp
-      (mem_filter.mp ha).1)).mp ((mem_filter.mp ha).2).symm,
-    symmetry,
-    rwa [(tsub_eq_iff_eq_add_of_le h), add_comm],
-    rw mem_filter,
-    have haσ : a ∈ range (card σ + 1) :=
-    by { rw mem_singleton.mp ha, exact mem_range_succ_iff.mpr (@tsub_le_self _ _ _ _ _ k) },
-    refine ⟨haσ, eq.symm _⟩,
-    rw tsub_eq_iff_eq_add_of_le (mem_range_succ_iff.mp haσ),
-    have hσ := (tsub_eq_iff_eq_add_of_le h).mp (mem_singleton.mp ha).symm,
-    rwa add_comm,
-  end,
-  simp only [prod_X_add_C_eval, ← esymm_to_sum, finset_sum_coeff, coeff_C_mul_X_pow, sum_ite, hk,
-    sum_singleton, esymm, eval_sum, eval_prod, eval_X, add_zero, sum_const_zero],
+  let s := (multiset.map (λ i : σ, (X i : mv_polynomial σ R)) finset.univ.val),
+  rw (_ : card σ = s.card) at ⊢ h,
+  { rw [esymm_eq_multiset.esymm σ R (s.card - k), finset.prod_eq_multiset_prod],
+    convert multiset.prod_X_add_C_coeff s h,
+    rwa multiset.map_map },
+  repeat { rw multiset.card_map, exact rfl, },
 end
 
 end mv_polynomial