support_zero

Mathlib.Algebra.DirectSum.Basic

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

English

Sum over the universal index set recovers the original direct sum element.

Русский

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

LaTeX

$$$\\sum_{i\\in \\mathrm{univ}} of\\,β_i\\,(x_i) = x$$$

Lean4

@[simp]
theorem support_zero [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] : (0 : ⨁ i, β i).support = ∅ :=
  DFinsupp.support_zero

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

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

Разделы

Аффилиация

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