finset.sum_add_distrib

Stream: maths

[Kevin Buzzard]

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]

sometimes you have to cycle through the list a couple times

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

Does that show anything?

[Kevin Buzzard]

sum_add.png nope

[Johan Commelin]

Meh... stupid programs

[Chris Hughes]

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

[Kevin Buzzard]

Begorrah you're right!