mathlib documentation

data.vector.zip

The zip_with operation on vectors. #

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

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

Equations
source
@[simp]
theorem vector.zip_with_to_list {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : vector α n) (y : vector β n) :
(vector.zip_with f x y).to_list = list.zip_with f x.to_list y.to_list
source
@[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)
source
@[simp]
theorem vector.zip_with_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : vector α n) (y : vector β n) :
(vector.zip_with f x y).tail = vector.zip_with f x.tail y.tail