The zipWith operation on vectors.

def List.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

• List.Vector.zipWith f x y = ⟨List.zipWith f ↑x ↑y, ⋯⟩

@[simp]

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

@[simp]

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

@[simp]

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

theorem List.Vector.prod_mul_prod_eq_prod_zipWith {α : Type u_1} {n : ℕ} [CommMonoid α] (x y : Vector α n) : x.toList.prod * y.toList.prod = (zipWith (fun (x1 x2 : α) => x1 * x2) x y).toList.prod

theorem List.Vector.sum_add_sum_eq_sum_zipWith {α : Type u_1} {n : ℕ} [AddCommMonoid α] (x y : Vector α n) : x.toList.sum + y.toList.sum = (zipWith (fun (x1 x2 : α) => x1 + x2) x y).toList.sum