finsupp sum of single

Stream: new members

[Lucas Viana Reis]

open finsupp

variables (α β γ : Type)
variables [has_zero β] [add_comm_monoid γ] {a : α} {b : β} (g : α → β → γ)
example : (single a b).sum g = g a b := by library_search

Hi, is this example in the library?

[Shing Tak Lam]

import data.finsupp.basic

variables (α β γ : Type)
variables [add_monoid β] [add_comm_monoid γ] {a : α} {b : β} (g : α → β → γ)

open finsupp

example (h : g a 0 = 0) : (single a b).sum g = g a b := finsupp.sum_single_index h

Note: [has_zero β] => [add_monoid β] and you need h : g a 0 = 0

[Lucas Viana Reis]

Thanks!

[Shing Tak Lam]

mhm... You don't need [add_comm_monoid β], here is a proof without (basically the same proof as sum_single_index)

import data.finsupp.basic

variables (α β γ : Type)
variables [has_zero β] [add_comm_monoid γ] {a : α} {b : β} (g : α → β → γ)

open finsupp

example (h : g a 0 = 0) : (single a b).sum g = g a b :=
begin
  by_cases hb : b = 0,
  { simp [h, hb, single_zero], refl },
  { simp [finsupp.sum, finsupp.support_single_ne_zero hb] }
end

[Lucas Viana Reis]

If b ≠ 0, do we still need the hypothesis g a 0 = 0?

[Shing Tak Lam]

no

example (h : b ≠ 0) : (single a b).sum g = g a b :=
begin
  simp [finsupp.sum, finsupp.support_single_ne_zero h]
end