Zulip Chat Archive

Stream: general

Topic: finset.sum_single


Morenikeji Neri (Jul 26 2018 at 18:28):

I'm wondering if there is a proof for
theorem finset.sum_single {α : Type}[fintype α ] {β : Type} [add_comm_monoid β] (f: α → β) {i: α} (h: ∀ (j:α), i ≠ j → f(j)=0 ):
f i = finset.sum finset.univ (λ (K: α),f K) := sorry
on mathlib?

Kevin Buzzard (Jul 26 2018 at 18:29):

rofl -- Keji did you just get internet? :-) Kenny proved this for you about 5 hours ago :-) The proof is in your email inbox :-)

Patrick Massot (Jul 26 2018 at 18:30):

You could also try to take up my dormant project https://github.com/PatrickMassot/bigop

Morenikeji Neri (Jul 26 2018 at 18:30):

Haha, yeah I did. I guess it waited to be sent when I wasn't connected . Thanks Kenny!


Last updated: Dec 20 2023 at 11:08 UTC