sum_zero_index

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.sum_zero_index

English

The sum over the zero element is zero: (0 : SkewMonoidAlgebra k G).sum f = 0.

Русский

Сумма по нулевому элементу равна нулю: (0 : SkewMonoidAlgebra k G).sum f = 0.

LaTeX

$$$\\big(0 : SkewMonoidAlgebra\\ k\\ G\\big).sum f = 0$$$

Lean4

@[simp]
theorem sum_zero_index {S : Type*} [AddCommMonoid S] {f : G → k → S} : (0 : SkewMonoidAlgebra k G).sum f = 0 := by
  simp [sum]

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

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

Разделы

Аффилиация

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