finset.sum over fin (n+1)

Stream: Is there code for X?

[Adam Topaz]

Do we have something like the following lemma?

lemma sum_eq {n} {α : Type*} [add_comm_monoid α] (ι : fin (n+1) → α) :
  (∑ (i : fin (n+1)), ι i) = ι 0 + ∑ i : fin n, ι i.succ := sorry

[Adam Topaz]

Scratch that, library search took a little while but found an answer :)

[Adam Topaz]

(it's docs#fin.sum_univ_succ in case anyone is curious)

[Scott Morrison]

(library_search runtime is linear in the number of declarations it has to look at, so running it in a separate file with smaller imports is often helpful. Of course, that risks leaving out the essential import.)