sum_zipWith_distrib_left — Mathlib

English

Given f and a, the sum of zipWith(a * f) over l1 and l2 equals a times the sum of zipWith f over l1 and l2.

Русский

Для f и a сумма zipWith(a·f) по l1 и l2 равна a умножить на сумму zipWith f по l1 и l2.

LaTeX

$$$\sum (zipWith (\"i j\" => a * f(i,j)) l1 l2) = a \cdot \left( \sum (zipWith f l1 l2) \right)$$$

Lean4

@[simp]
theorem sum_zipWith_distrib_left [NonUnitalNonAssocSemiring R] (f : ι → κ → R) (a : R) :
    ∀ (l₁ : List ι) (l₂ : List κ), (zipWith (fun i j ↦ a * f i j) l₁ l₂).sum = a * (zipWith f l₁ l₂).sum
  | [], _ => by simp
  | _, [] => by simp
  | i :: l₁, j :: l₂ => by simp [sum_zipWith_distrib_left, mul_add]

Похожие утверждения