mathlib documentation

data.vector.zip

The zip_with operation on vectors. #

def vector.zip_with {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : α → β → γ) :
vector α nvector β nvector γ n

Apply the function f : α → β → γ to each corresponding pair of elements from two vectors.

Equations
@[simp]
theorem vector.zip_with_to_list {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : α → β → γ) (x : vector α n) (y : vector β n) :
@[simp]
theorem vector.zip_with_nth {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : α → β → γ) (x : vector α n) (y : vector β n) (i : fin n) :
(vector.zip_with f x y).nth i = f (x.nth i) (y.nth i)
@[simp]
theorem vector.zip_with_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : α → β → γ) (x : vector α n) (y : vector β n) :