sum_map_mul_right

Mathlib.Algebra.BigOperators.Ring.List

URI: https://scilib.ai/kg/mathlib#List.sum_map_mul_right

English

For a list l and functions f, r, the sum of r multiplied by f over l equals r times the sum of f over l.

Русский

Для списка l и функций f, r сумма r·f над l равна r умножить на сумму f над l.

LaTeX

$$$\sum_{b\in l} (r \cdot f(b)) = r \cdot \left( \sum_{b\in l} f(b) \right)$$$

Lean4

theorem sum_map_mul_right : (l.map fun b ↦ f b * r).sum = (l.map f).sum * r :=
  sum_map_hom l f <| AddMonoidHom.mulRight r

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru