Sum over product set

Stream: new members

[Pim Otte]

I'm trying to state the equality from exercise 1 here. This involves a sum over all vectors {-1,1}^d. How do I formulate this? I think finset.pi is the thing I should be using, but it seems a little overkill at some points, but I have some trouble grasping the definition in general. It also seems to not be used anywhere else in the library, so I might be on the wrong track. Any pointers?

import data.mv_polynomial.basic
import data.complex.basic
import ring_theory.polynomial.homogeneous

noncomputable theory

open_locale big_operators

open mv_polynomial


def polynomial_identity {R : Type*} [comm_semiring R] (d : ℕ) : (∏ i, (X i): mv_polynomial (fin d) R) = ∑ α in (finset.pi (fin d) ((λ _, (fin 2)))), (X 0) :=
begin
end

[Eric Wieser]

finset.pi is used behind the scenes when you write ∑ f : fin d → ℤˣ, ...

[Eric Wieser]

(by docs#pi.fintype)

[Eric Wieser]

(also, ℤˣ is likely a better translation of {1,-1} than fin 2)

[Pim Otte]

@Eric Wieser Thanks! That's very helpful:)