sum_def'

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.sum_def'

Lean4

/-- Unfolded version of `sum_def` in terms of `Finset.sum`. -/
theorem sum_def' {N : Type*} [AddCommMonoid N] (f : SkewMonoidAlgebra k G) (g : G → k → N) :
    sum f g = ∑ a ∈ f.support, g a (f.coeff a) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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