## Stream: maths

### Topic: finset.sum_add_distrib

#### Kevin Buzzard (Jan 30 2020 at 11:19):

A student just asked me how to prove $\Sigma_{i\in I}(a_i+b_i)=\Sigma_i a_i + \Sigma_i b_i$ in Lean. I said "it will be called finset.sum_add". We tried, and it wasn't. The VS Code ctrl-space dance gave me nothing after rw finset.sum_add either, or #check finset.sum_add. We have algebra.big_operators imported. So of course I knew it would be there, so I went to the definition of finset.sum and looked around, and it's called finset.sum_add_distrib. I would have expected ctrl-space to find this -- why does it not? This has wasted some of my student's time. Is it something to do with the fact that the result was generated by [to_additive]?

#### Mario Carneiro (Jan 30 2020 at 11:20):

sometimes you have to cycle through the list a couple times

#### Kevin Buzzard (Jan 30 2020 at 11:20):

I'm only too aware of this, but I couldn't even get that to work in this case.

#### Johan Commelin (Jan 30 2020 at 11:22):

How about Ctrl-P and then #finset.sum_add?

#### Johan Commelin (Jan 30 2020 at 11:22):

Does that show anything?

sum_add.png nope

#### Johan Commelin (Jan 30 2020 at 11:29):

Meh... stupid programs

#### Chris Hughes (Jan 30 2020 at 12:15):

If you have the finset namespace open then it doesn't work.

#### Kevin Buzzard (Jan 30 2020 at 13:01):

Begorrah you're right!

Last updated: May 09 2021 at 10:11 UTC