sum_map_mul_right — Mathlib

English

Let R be a non-unital non-assoc semiring. For any a ∈ R and any f: ι → R, the sum of f(i) multiplied on the right by a equals the sum times a: ∑_{i∈s} (f(i) · a) = (∑_{i∈s} f(i)) · a.

Русский

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

LaTeX

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

Lean4

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

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