coe_lsum

Mathlib.LinearAlgebra.Finsupp.LSum

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

English

The map lsum composed with the finsupp singleton map equals the original map f on M.

Русский

Композиция lsum с lsingle оставляет неизменной исходную карту f на M.

LaTeX

$$$$ \mathrm{lsum}_S f \circ \mathrm{lsingle}_i = f_i. $$$$

Lean4

@[simp]
theorem coe_lsum (f : α → M →ₛₗ[σ] N) : (lsum S f : (α →₀ M) → N) = fun d => d.sum fun i => f i :=
  rfl

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

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

Разделы

Аффилиация

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