English
The underlying List of scanl equals the List.scanl of the underlying List of the original vector.
Русский
Подлежащее представление scanl равно List.scanl от исходного списка вектора.
LaTeX
$$$\\forall {v:\\mathrm{Vector}\\ \\alpha\\ n},\\; (\\mathrm{scanl}(f,b,v)).\\mathrm{val} = \\mathrm{List.scanl}(f,b,v.\\mathrm{val})$$$
Lean4
/-- The underlying `List` of a `Vector` after a `scanl` is the `List.scanl`
of the underlying `List` of the original `Vector`.
-/
@[simp]
theorem scanl_val : ∀ {v : Vector α n}, (scanl f b v).val = List.scanl f b v.val
| _ => rfl