lsingle — Mathlib

English

The theorem dfinsuppSum_apply expresses that the coefficient-wise sum of linear maps applied to b equals the sum of the maps applied to b term-wise.

Русский

Теорема dfinsuppSum_apply устанавливает, что сумма линейных отображений по коэффициентам действует на b поэтапно как сумма отдельных отображений на b.

LaTeX

$$$ (t.sum g) b = t.sum (\lambda i d, g i d b)$$$

Lean4

/-- Interpret `Finsupp.single a` as a linear map. -/
def lsingle (a : α) : M →ₗ[R] α →₀ M :=
  { Finsupp.singleAddHom a with map_smul' := fun _ _ => (smul_single _ _ _).symm }

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