Documentation

Mathlib.Data.Vector.Zip

The zipWith operation on vectors. #

def Mathlib.Vector.zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : αβγ) :

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

Equations
Instances For
    @[simp]
    theorem Mathlib.Vector.zipWith_toList {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : αβγ) (x : Mathlib.Vector α n) (y : Mathlib.Vector β n) :
    (Mathlib.Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList
    @[simp]
    theorem Mathlib.Vector.zipWith_get {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : αβγ) (x : Mathlib.Vector α n) (y : Mathlib.Vector β n) (i : Fin n) :
    (Mathlib.Vector.zipWith f x y).get i = f (x.get i) (y.get i)
    @[simp]
    theorem Mathlib.Vector.zipWith_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (f : αβγ) (x : Mathlib.Vector α n) (y : Mathlib.Vector β n) :
    (Mathlib.Vector.zipWith f x y).tail = Mathlib.Vector.zipWith f x.tail y.tail
    theorem Mathlib.Vector.sum_add_sum_eq_sum_zipWith {α : Type u_1} {n : } [AddCommMonoid α] (x : Mathlib.Vector α n) (y : Mathlib.Vector α n) :
    x.toList.sum + y.toList.sum = (Mathlib.Vector.zipWith (fun (x x_1 : α) => x + x_1) x y).toList.sum
    theorem Mathlib.Vector.prod_mul_prod_eq_prod_zipWith {α : Type u_1} {n : } [CommMonoid α] (x : Mathlib.Vector α n) (y : Mathlib.Vector α n) :
    x.toList.prod * y.toList.prod = (Mathlib.Vector.zipWith (fun (x x_1 : α) => x * x_1) x y).toList.prod