## Stream: maths

### Topic: Sums over finsets

#### Johan Commelin (May 22 2018 at 14:09):

I'm stuck on the following triviality

lemma sums {m n : ℕ} (f : fin m → fin n) (x : fin m → ℕ)
: sum univ (λ j : fin n, sum (univ.filter (λ i, f i = j)) x) = sum univ x
:= sorry


It looks like I might want to use finset.sum_sigma but I don't see how to get all the sigma's in place. And the unification magic doesn't do the job either.

#### Johan Commelin (May 22 2018 at 14:10):

@Kevin Buzzard @Chris Hughes I remember that you were also working on these kind of sum-rewritings about 2 months ago. Is this similar to what you did?

#### Johannes Hölzl (May 22 2018 at 14:18):

you can use finset.sum_bind to combine both sum to a single one and then use extensionality that the combination of the index sets on the right is univ. Or use finset.sum_subset which also uses some sort of extensionality.

Ok, thanks!

#### Johan Commelin (May 22 2018 at 17:20):

Ok, I proved the lemma using bind and ext.2. Thanks a lot!

Last updated: May 11 2021 at 15:12 UTC