# Documentation

Mathlib.Data.Vector.Zip

# The zipWith operation on vectors. #

def Vector.zipWith {α : 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.zipWith_toList {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : αβγ) (x : Vector α n) (y : Vector β n) :
@[simp]
theorem Vector.zipWith_get {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : αβγ) (x : Vector α n) (y : Vector β n) (i : Fin n) :
Vector.get () i = f () ()
@[simp]
theorem Vector.zipWith_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : αβγ) (x : Vector α n) (y : Vector β n) :
theorem Vector.sum_add_sum_eq_sum_zipWith {α : Type u_1} {n : } [inst : ] (x : Vector α n) (y : Vector α n) :
= List.sum (Vector.toList (Vector.zipWith (fun x x_1 => x + x_1) x y))
theorem Vector.prod_mul_prod_eq_prod_zipWith {α : Type u_1} {n : } [inst : ] (x : Vector α n) (y : Vector α n) :
= List.prod (Vector.toList (Vector.zipWith (fun x x_1 => x * x_1) x y))