sum_single

Mathlib.Algebra.MonoidAlgebra.Defs

URI: https://scilib.ai/kg/mathlib#MonoidAlgebra.sum_single

English

For any x ∈ MonoidAlgebra R M, x.sum single = x; i.e., summing the basis elements reconstructs x.

Русский

Для любого x ∈ MonoidAlgebra R M выполняется x.sum single = x; суммирование базисных элементов восстанавливает x.

LaTeX

$$$ x.sum\\, single = x $$$

Lean4

@[to_additive (attr := simp)]
theorem sum_single (x : MonoidAlgebra R M) : x.sum single = x :=
  Finsupp.sum_single _

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

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

Разделы

Аффилиация

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