Help with mv_polynomial

Stream: new members

[María Inés de Frutos Fernández]

I'm having trouble using the new mv_polynomial.prod_X_add_C_coeff. What would I have to use instead of the last rw in this mwe?

import ring_theory.polynomial.vieta

open polynomial
lemma polynomial.prod_X_sub_C_coeff {K : Type*} [field K]  {n : ℕ} (hn : 0 < n) (b : fin n → K)
  {m : ℕ} (hm : m ≤ n) : (finprod (λ (k : fin n), polynomial.X - (polynomial.C (b k)))).coeff m =
  (finset.powerset_len (n - m) finset.univ).sum
    (λ (t : finset (fin n)), t.prod (λ (i : (fin n)), - b i)) :=
begin
  simp_rw [sub_eq_add_neg, ← polynomial.C_neg, ← pi.neg_apply],
  rw [finprod_eq_prod_of_fintype],
  rw mv_polynomial.prod_X_add_C_coeff, -- now fails because the LHS of this lemma has changed
  sorry
end

[Adam Topaz]

docs#mv_polynomial.prod_X_add_C_coeff

[Adam Topaz]

It seems like the goal at that point is

(finset.univ.prod (λ (i : fin n), X + ⇑C ((-b) i))).coeff m =
  (finset.powerset_len (n - m) finset.univ).sum (λ (x : finset (fin n)), x.prod (λ (x : fin n), (-b) x))

and the LHS doesn't match the LHS of the lemma because of the -b (as opposed to mv_polynomial.X).
Am I just confused?

[María Inés de Frutos Fernández]

Yes, that's what's going on - the old prod_X_add_C_coeff, which was modified to mv_polynomial.prod_X_add_C_coeff in #15008, was

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 :=

The new version seems more general, but I can't figure out how to apply it to prove the goal above.

[Xavier Roblot]

For this kind of situation, you might want to use the new docs#multiset.prod_X_sub_C_coeff which is more flexible.

[María Inés de Frutos Fernández]

Ok, I'll check it out. Thanks!

[Junyan Xu]

@María Inés de Frutos Fernández You can prove it this way:

import ring_theory.polynomial.vieta

lemma finset.esymm_map_val {σ R} [comm_semiring R] (f : σ → R) (s : finset σ) (n : ℕ) :
  (s.val.map f).esymm n = (s.powerset_len n).sum (λ t, t.prod f) :=
begin
  rw [multiset.esymm, multiset.powerset_len_map, ← finset.map_val_val_powerset_len],
  simpa only [multiset.map_map],
end

open polynomial
lemma polynomial.prod_X_sub_C_coeff {K : Type*} [field K]  {n : ℕ} (hn : 0 < n) (b : fin n → K)
  {m : ℕ} (hm : m ≤ n) : (finprod (λ (k : fin n), polynomial.X - (polynomial.C (b k)))).coeff m =
  (finset.powerset_len (n - m) finset.univ).sum
    (λ (t : finset (fin n)), t.prod (λ (i : (fin n)), - b i)) :=
begin
  simp_rw [sub_eq_add_neg, ← polynomial.C_neg, ← pi.neg_apply],
  rw [finprod_eq_prod_of_fintype],
  rw finset.prod_eq_multiset_prod,
  rw ← multiset.map_map (λ x : K, X + C x) (-b),
  have : (finset.univ.val.map (-b)).card = n,
  { rw multiset.card_map, exact finset.card_fin n },
  rw multiset.prod_X_add_C_coeff,
  { rw finset.esymm_map_val, congr, exact this },
  { rw this, exact hm },
end

[Junyan Xu]

I've PR'd the lemma finset.esymm_map_val and use it to golf an existing proof: #16424

[María Inés de Frutos Fernández]

Thanks!