Theorems · Theorem · combinatorics

List.Vector.scanl_cons

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

The recursive step of scanl splits a vector x ::ᵥ v : Vector α (n + 1) into the provided starting value b : β and the recursed scanl f b x : β as the starting value. This lemma is the cons version of scanl_get.

Defined in

Mathlib.Data.Vector.Basic

Cited by

3 results in Mathlib

Foundations

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