The zip_with operation on vectors. #
Apply the function f : α → β → γ to each corresponding pair of elements from two vectors.
Equations
- vector.zip_with f = λ (x : vector α n) (y : vector β n), ⟨list.zip_with f x.val y.val, _⟩
@[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
@[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
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
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