Zulip Chat Archive

Stream: maths

Topic: finset.sum_add_distrib


view this post on Zulip Kevin Buzzard (Jan 30 2020 at 11:19):

A student just asked me how to prove ΣiI(ai+bi)=Σiai+Σibi\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]?

view this post on Zulip Mario Carneiro (Jan 30 2020 at 11:20):

sometimes you have to cycle through the list a couple times

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jan 30 2020 at 11:22):

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

view this post on Zulip Johan Commelin (Jan 30 2020 at 11:22):

Does that show anything?

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 11:24):

sum_add.png nope

view this post on Zulip Johan Commelin (Jan 30 2020 at 11:29):

Meh... stupid programs

view this post on Zulip Chris Hughes (Jan 30 2020 at 12:15):

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

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 13:01):

Begorrah you're right!


Last updated: May 09 2021 at 10:11 UTC