finset.sum_single

Stream: general

[Morenikeji Neri]

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]

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]

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

[Morenikeji Neri]

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