lsum_apply

Mathlib.LinearAlgebra.Finsupp.LSum

URI: https://scilib.ai/kg/mathlib#Finsupp.lsum_apply

English

A variant of the previous with the general form showing the compatibility with lsingle and lsum.

Русский

Вариант предыдущего с общей формой совместимости с lsingle и lsum.

LaTeX

$$$$ (Finsupp.lsum S f) \circ (Finsupp.lsingle x) = f x. $$$$

Lean4

theorem lsum_apply (f : α → M →ₛₗ[σ] N) (l : α →₀ M) : Finsupp.lsum S f l = l.sum fun b => f b :=
  rfl

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

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

Разделы

Аффилиация

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