Apply the function f : α → β → γ
to each corresponding pair of elements from two vectors.
Equations
- Vector.zipWith f x y = ⟨List.zipWith f ↑x ↑y, ⋯⟩
Instances For
@[simp]
theorem
Vector.zipWith_toList
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{n : ℕ}
(f : α → β → γ)
(x : Vector α n)
(y : Vector β n)
:
(Vector.zipWith f x y).toList = List.zipWith f x.toList y.toList
@[simp]
theorem
Vector.zipWith_tail
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{n : ℕ}
(f : α → β → γ)
(x : Vector α n)
(y : Vector β n)
:
(Vector.zipWith f x y).tail = Vector.zipWith f x.tail y.tail
theorem
Vector.sum_add_sum_eq_sum_zipWith
{α : Type u_1}
{n : ℕ}
[AddCommMonoid α]
(x : Vector α n)
(y : Vector α n)
:
x.toList.sum + y.toList.sum = (Vector.zipWith (fun (x x_1 : α) => x + x_1) x y).toList.sum
theorem
Vector.prod_mul_prod_eq_prod_zipWith
{α : Type u_1}
{n : ℕ}
[CommMonoid α]
(x : Vector α n)
(y : Vector α n)
:
x.toList.prod * y.toList.prod = (Vector.zipWith (fun (x x_1 : α) => x * x_1) x y).toList.prod