Zulip Chat Archive

Stream: new members

Topic: add one more to sum


Alex Kontorovich (Apr 10 2020 at 20:49):

Hi all, is there a tactic that just takes care of this? \sum_{i<n+1}a(i) = \sum_{i<n}a(i) + a(n) Thanks!

lemma sum_succ_is_add_last_term (a:ℕ→α )( n: ):
(sum (range (n+1)) a = sum (range n) a + a (n+1))
:=
sorry,

Kenny Lau (Apr 10 2020 at 20:50):

sum_range_succ

Patrick Massot (Apr 10 2020 at 20:52):

He asked for a tactic. The answer is thus library_search.

Alex Kontorovich (Apr 10 2020 at 20:54):

Perfect, thanks! (What is library_search? Something where I could've found this on my own?)

Patrick Massot (Apr 10 2020 at 20:55):

Try replacing this sorry, by by library_search.

PV (Apr 10 2020 at 22:24):

do you have to do anything special to make that work in the web viewer?

Kevin Buzzard (Apr 10 2020 at 22:28):

you have to use the right web viewer. The official Lean one has a very old mathlib. The one I link to has a bang up to date one, thanks to the amazing efforts of the leanprover-community people. Oh -- you also need to import tactic.

PV (Apr 10 2020 at 22:42):

ahh thanks.

Bryan Gin-ge Chen (Apr 10 2020 at 22:48):

What is library_search? Something where I could've found this on my own?

Here it is in the mathlib tactic docs. See also suggest.


Last updated: Dec 20 2023 at 11:08 UTC