sum_support_of

Mathlib.Algebra.DirectSum.Basic

URI: https://scilib.ai/kg/mathlib#DirectSum.sum_support_of

English

Summing the values along all components recovers the whole direct sum element.

Русский

Суммирование по всем компонентам восстанавливает элемент прямой суммы.

LaTeX

$$$\\sum_{i} of\\;β_i\\,(x_i) = x$$$

Lean4

theorem sum_support_of [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (x : ⨁ i, β i) : (∑ i ∈ x.support, of β i (x i)) = x :=
  DFinsupp.sum_single

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

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

Разделы

Аффилиация

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