Theorems · Theorem · combinatorics

List.Vector.scanl_head

∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α n),
  (List.Vector.scanl f b v).head = b

The first element of scanl of a vector v : Vector α n, retrieved via head, is the starting value b : β.

Defined in

Mathlib.Data.Vector.Basic

Cited by

1 results in Mathlib

Foundations

Depth 48 from the axioms · uses propext, Quot.sound