def
Mathlib.Vector.zipWith
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{n : ℕ}
(f : α → β → γ)
:
Mathlib.Vector α n → Mathlib.Vector β n → Mathlib.Vector γ n
Apply the function f : α → β → γ to each corresponding pair of elements from two vectors.
Equations
- Mathlib.Vector.zipWith f x y = ⟨List.zipWith f ↑x ↑y, ⋯⟩
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.prod_mul_prod_eq_prod_zipWith
{α : Type u_1}
{n : ℕ}
[CommMonoid α]
(x y : Mathlib.Vector α n)
:
x.toList.prod * y.toList.prod = (Mathlib.Vector.zipWith (fun (x1 x2 : α) => x1 * x2) x y).toList.prod
theorem
Mathlib.Vector.sum_add_sum_eq_sum_zipWith
{α : Type u_1}
{n : ℕ}
[AddCommMonoid α]
(x y : Mathlib.Vector α n)
:
x.toList.sum + y.toList.sum = (Mathlib.Vector.zipWith (fun (x1 x2 : α) => x1 + x2) x y).toList.sum