sum_sum

Stream: Is there code for X?

[Yakov Pechersky]

I can't find the finset sum lemma that is the association that makes this work, and guessing the name isn't working either. What am I missing?

import data.polynomial.basic

open polynomial

lemma sum_sum {R S T : Type*} [semiring R] [semiring S] [add_comm_monoid T]
  (p : polynomial R) (f : ℕ → R → polynomial S) (g : ℕ → S → T) :
  (p.sum f).sum g = p.sum (λ i a, (f i a).sum g) :=
begin
  simp_rw sum_def,
  sorry,
end

[Yakov Pechersky]

Feel free to place any add_monoid_hom requirements as necessary.

[Yakov Pechersky]

Seems like for my purposes, it's easier to just induct on the polynomial instead of juggling between sum and lsum, coeff and lcoeff.

[Eric Wieser]

docs#finsupp.sum_comm?

[Eric Wieser]

After the usual "unfold the polynomial to add_monoid_algebra" boilerplate

[Yakov Pechersky]

That's not exactly what I want. Take a look at #11139, #sum_taylor_eq

[Ashvni Narayanan]

(deleted)