coefft of X^j in prod_i (X + a_i)

Stream: Is there code for X?

[Kevin Buzzard]

I don't care what the sum is over (I don't know whether .to_finset is horrible to prove things about), but a student at Xena is working on Newton's identities and this comes up. Do we have anything like it? All we need is that the coefficient is an R-linear combination of the products but I guess the natural thing to do is to prove that it's equal to the sum of them.

import data.polynomial.coeff

open polynomial

open_locale big_operators

variables (S : Type*) [fintype S] (R : Type*) [comm_ring R] (a : S → R)

-- Want: coefficient of X^j in ∏_{i ∈ S} (X + a_i) is the obvious thing
example (j : ℕ) (hj : j ≤ fintype.card S) : (∏ i : S, (X + C (a i))).coeff j =
  ∑ s in ({s : finset S | s.card = fintype.card S - j}.to_finset), ∏ k in s, a k :=
begin
  sorry
end

[Adam Topaz]

there must be something like this, given that we have a good amount of Galois theory.

[Adam Topaz]

but my search comes up short, unfortunately.

[Adam Topaz]

Is this it? docs#multiset.prod_X_sub_C_coeff

[Kevin Buzzard]

Thanks! Indeed the finset version is too weak. I didn't check that file, I must be honest ;-)

[Adam Topaz]

It took me a little while to understand what that theorem was even saying...

[Adam Topaz]

Why doesn't it render as s.map ... on the webpage?

[Eric Wieser]

I suspect the webpage printing uses the stricter version of dot notation that needs the argument in the first position