sum_zero

Mathlib.Algebra.BigOperators.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.sum_zero

English

If you sum a finitely supported function with zeros everywhere, you get the zero element.

Русский

Если сумму конечной опоры функции взять с нулями, получится ноль.

LaTeX

$$$$ \bigl(f \sum (\lambda a b, 0)\bigr) = 0. $$$$

Lean4

@[simp]
theorem sum_zero [Zero M] [AddCommMonoid N] {f : α →₀ M} : (f.sum fun _ _ => (0 : N)) = 0 :=
  Finset.sum_const_zero

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

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

Разделы

Аффилиация

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