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.

source
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
source
@[simp]
theorem vector.zip_with_to_list {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : vector α n) (y : vector β n) :
(vector.zip_with f x y).to_list = list.zip_with f x.to_list y.to_list
source
@[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)
source
@[simp]
theorem vector.zip_with_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (f : α → β → γ) (x : vector α n) (y : vector β n) :
(vector.zip_with f x y).tail = vector.zip_with f x.tail y.tail
source
theorem vector.prod_mul_prod_eq_prod_zip_with {α : Type u_1} {n : ℕ} [comm_monoid α] (x y : vector α n) :
x.to_list.prod * y.to_list.prod = (vector.zip_with has_mul.mul x y).to_list.prod
source
theorem vector.sum_add_sum_eq_sum_zip_with {α : Type u_1} {n : ℕ} [add_comm_monoid α] (x y : vector α n) :
x.to_list.sum + y.to_list.sum = (vector.zip_with has_add.add x y).to_list.sum