The zipWith operation on vectors.

def Vector.zipWith {α : 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

• Vector.zipWith f x y = { val := List.zipWith f ↑x ↑y, property := (_ : List.length (List.zipWith f ↑x ↑y) = n) }

@[simp]

theorem Vector.zipWith_toList {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : Vector α n) (y : Vector β n) : Vector.toList (Vector.zipWith f x y) = List.zipWith f (Vector.toList x) (Vector.toList y)

@[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 (Vector.zipWith f x y) i = f (Vector.get x i) (Vector.get y i)

@[simp]

theorem Vector.zipWith_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : Vector α n) (y : Vector β n) : Vector.tail (Vector.zipWith f x y) = Vector.zipWith f (Vector.tail x) (Vector.tail y)

theorem Vector.sum_add_sum_eq_sum_zipWith {α : Type u_1} {n : ℕ} [AddCommMonoid α] (x : Vector α n) (y : Vector α n) : List.sum (Vector.toList x) + List.sum (Vector.toList y) = 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 : ℕ} [CommMonoid α] (x : Vector α n) (y : Vector α n) : List.prod (Vector.toList x) * List.prod (Vector.toList y) = List.prod (Vector.toList (Vector.zipWith (fun (x x_1 : α) => x * x_1) x y))