English
For i : Fin n, the (i+1)-th element of scanl equals f of the (i cast) element of scanl with the i-th element of v.
Русский
Для i : Fin n, элемент i.succ у scanl равен f( element_i_cast, element_i(v) ).
LaTeX
$$$\\forall {i : \\mathrm{Fin} n},\\; (\\mathrm{scanl}(f,b,v)).get(i).succ = f((\\mathrm{scanl}(f,b,v).get(i^{\\mathrm{cast}})) , v.get(i))$$$
Lean4
/-- The first element of `scanl` of a vector `v : Vector α n`,
retrieved via `head`, is the starting value `b : β`.
-/
@[simp]
theorem scanl_head : (scanl f b v).head = b := by
cases n
· have : v = nil := by simp only [eq_iff_true_of_subsingleton]
simp only [this, scanl_nil, head_cons]
· rw [← cons_head_tail v]
simp [← get_zero, get_eq_get_toList]
