feat(ring_theory/polynomial/symmetric): restore finset.powerset_len…

… version of `prod_X_sub_C_coeff` (#16424)

In #15008, [`prod_X_add_C_coeff`](https://github.com/leanprover-community/mathlib/pull/15008/files#diff-08ead07a5e3b20f4db52e932b309a2ff767e486e4a0bf7d90b5520d25d95dc57L79-L81) was changed to use `multiset.esymm` in its RHS, which is defined in terms of `multiset.powerset_len` and not defeq to the original version which involves `finset.powerset_len` instead. This PR restores the `finset` version by introducing `finset.esymm_map_val`, a generalized version of `mv_polynomial.esymm_eq_multiset_esymm` (this lemma is renamed from `mv_polynomial.esymm_eq_multiset.esymm` to better conform with mathlib convention).

Co-authored-by: negiizhao <egresf@gmail.com>

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Help.20with.20mv_polynomial/near/297702031)



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

src/ring_theory/polynomial/symmetric.lean

@@ -51,6 +51,10 @@ 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
 
+lemma _root_.finset.esymm_map_val {σ} (f : σ → R) (s : finset σ) (n : ℕ) :
+  (s.val.map f).esymm n = (s.powerset_len n).sum (λ t, t.prod f) :=
+by simpa only [esymm, powerset_len_map, ← finset.map_val_val_powerset_len, map_map]
+
 end multiset
 
 namespace mv_polynomial
@@ -132,14 +136,12 @@ def esymm (n : ℕ) : mv_polynomial σ R :=
 
 /-- 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
+lemma esymm_eq_multiset_esymm : esymm σ R = (finset.univ.val.map X).esymm :=
+funext $ λ n, (finset.univ.esymm_map_val X n).symm
+
+lemma aeval_esymm_eq_multiset_esymm [algebra R S] (f : σ → S) (n : ℕ) :
+  aeval f (esymm σ R n) = (finset.univ.val.map f).esymm n :=
+by simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]
 
 /-- 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 =

src/ring_theory/polynomial/vieta.lean

@@ -68,6 +68,14 @@ begin
     exact nat.sub_lt_succ s.card k }
 end
 
+lemma prod_X_add_C_coeff' {σ} (s : multiset σ) (r : σ → R) {k : ℕ} (h : k ≤ s.card) :
+  (s.map (λ i, X + C (r i))).prod.coeff k = (s.map r).esymm (s.card - k) :=
+by rw [← map_map (λ r, X + C r) r, prod_X_add_C_coeff]; rwa s.card_map r
+
+lemma _root_.finset.prod_X_add_C_coeff {σ} (s : finset σ) (r : σ → R) {k : ℕ} (h : k ≤ s.card) :
+  (∏ i in s, (X + C (r i))).coeff k = ∑ t in s.powerset_len (s.card - k), ∏ i in t, r i :=
+by { rw [finset.prod, prod_X_add_C_coeff' _ r h, finset.esymm_map_val], refl }
+
 end semiring
 
 section ring
@@ -142,21 +150,21 @@ lemma mv_polynomial.prod_C_add_X_eq_sum_esymm :
 begin
   let s := finset.univ.val.map (λ i : σ, mv_polynomial.X i),
   rw (_ : card σ = s.card),
-  { simp_rw [mv_polynomial.esymm_eq_multiset.esymm σ R _, finset.prod_eq_multiset_prod],
+  { simp_rw [mv_polynomial.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, }
+  { rw multiset.card_map, refl, }
 end
 
 lemma mv_polynomial.prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ) :
   (∏ i : σ, (X + C (mv_polynomial.X i))).coeff k = mv_polynomial.esymm σ R (card σ - k) :=
 begin
   let s := finset.univ.val.map (λ i, (mv_polynomial.X i : mv_polynomial σ R)),
   rw (_ : card σ = s.card) at ⊢ h,
-  { rw [mv_polynomial.esymm_eq_multiset.esymm σ R (s.card - k), finset.prod_eq_multiset_prod],
+  { rw [mv_polynomial.esymm_eq_multiset_esymm σ R, 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, },
+  repeat { rw multiset.card_map, refl, },
 end
 
 end mv_polynomial