sum_map_mul_left — Mathlib

English

Let R be a non-unital non-associative semiring. For any a in R and any function f: ι → R, the sum over s of the products a * f(i) equals a times the sum of f(i): ∑_{i∈s} a · f(i) = a · ∑_{i∈s} f(i).

Русский

Пусть R — полусемиринг без единицы и без ассоциативности. Для любого a ∈ R и любой функции f: ι → R верно: сумма по s элементов a · f(i) равна a · сумма по s элементов f(i).

LaTeX

$$$$ \sum_{i \in s} (a \cdot f(i)) = a \cdot \sum_{i \in s} f(i). $$$$

Lean4

theorem sum_map_mul_left : sum (s.map fun i ↦ a * f i) = a * sum (s.map f) :=
  Multiset.induction_on s (by simp) fun i s ih => by simp [ih, mul_add]

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