finset.sum_add

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is the lemma below in mathlib? If not, should it be?

Thanks!

import algebra.big_operators.basic

open finset
open_locale big_operators

variables {α β : Type*}

lemma finset.sum_add [add_comm_monoid β] {F G : α → β} (s : finset α) :
  ∑ x in s, (F x + G x) = ∑ x in s, F x + ∑ x in s, G x :=
begin
  classical,
  refine finset.induction_on s (by simp) (λ a s as h, _),
  rw [sum_insert as, sum_insert as, sum_insert as, h],
  rw [add_assoc, add_comm (G a), add_comm (G a), ← add_assoc, ← add_assoc, ← add_assoc],
end

[Scott Morrison]

import algebra.big_operators.basic

open finset
open_locale big_operators

variables {α β : Type*}

lemma finset.sum_add [add_comm_monoid β] {F G : α → β} (s : finset α) :
  ∑ x in s, (F x + G x) = ∑ x in s, F x + ∑ x in s, G x :=
by library_search -- sum_add_distrib

[Damiano Testa]

Thanks!

I tried library_search, but nothing came up. Maybe it was because I was in lean_liquid.

[Joseph Hua]

By the way the right thing to do is to prove the same statement finset.mul_prod for a comm_monoid, and then give it the attribute @[to_additive] as is done here https://github.com/leanprover-community/mathlib/blob/d6a8e5d7dc12a8d39dec34221009e244c141529c/src/algebra/big_operators/basic.lean#L1195