mathlib3 documentation

data.vector.zip

The zip_with operation on vectors. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[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) :