combining two sums into one

Stream: new members

[Emma R. Hasson]

One more problem- (thanks for your help!) how to change between summing over products and summing over pairs?

example (f : ℝ×ℝ → ℝ) (s t : finset ℝ) :
  ∑ x in s, ∑ y in t, f ⟨x, y⟩ =  ∑ x in (s.product t), f x  :=
begin
  sorry
end

[Eric Wieser]

My guess of the name would be docs#finset.sum_product

[Eric Wieser]

Indeed, that's your statement but reversed

[Eric Wieser]

Did you try library_search?

[Emma R. Hasson]

Yup that worked! I did try library_search but it didn't return anything.