Zulip Chat Archive

Stream: maths

Topic: proof about sums


view this post on Zulip Chris Hughes (Oct 12 2019 at 17:14):

What is the correct proof of this? It can be done in short way using definitional unfolding, but this isn't very stable.

example {α : Type*} [add_comm_monoid α] (f : fin 4 → α) :
  univ.sum f = f 0 + f 1 + f 2 + f 3

view this post on Zulip Kenny Lau (Oct 12 2019 at 18:08):

import data.fintype

open finset

example {α : Type*} [add_comm_monoid α] (f : fin 4  α) :
  univ.sum f = f 0 + f 1 + f 2 + f 3 :=
have huniv : (univ : finset (fin 4)).val = 0::1::2::3::0, from dec_trivial,
show multiset.sum _ = _,
by rw huniv; simp only [multiset.map_cons, multiset.map_zero, multiset.sum_cons, multiset.sum_zero];
rw add_zero; iterate 2 { rw  add_assoc }

view this post on Zulip Kenny Lau (Oct 12 2019 at 18:10):

I mean, the f 0 + f 1 + f 2 + f 3 part isn't very clearly generalizable. (clearly it isn't list.sum (list.range 4) f)


Last updated: May 11 2021 at 16:22 UTC