Theorems · Theorem · combinatorics

List.Vector.scanl_get

∀ {α : Type u_1} {n : ℕ} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α n) (i : Fin n),
  (List.Vector.scanl f b v).get i.succ = f ((List.Vector.scanl f b v).get i.castSucc) (v.get i)

For an index i : Fin n, the nth element of scanl of a vector v : Vector α n at i.succ, is equal to the application function f : β → α → β of the castSucc i element of scanl f b v and get v i. This lemma is the get version of scanl_cons.

Defined in

Mathlib.Data.Vector.Basic

Cited by

0 results in Mathlib

Foundations

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