coe_finsupp_sum — Mathlib

English

The coercion to a linear map commutes with finsupp sums: the function t.sum g, viewed as a linear map, equals the sum of the linear maps g i d.

Русский

Приведение к линейному отображению аккуратно распределяет сумму finsupp: коe функции t.sum g равна интеграции линейных отображений g i d.

LaTeX

$$$\operatorname{coe}\,(t.sum\,g) = t.sum\,\big(\lambda i d, \operatorname{coe}\,(g(i,d))\big)$$$

Lean4

theorem coe_finsupp_sum (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) : ⇑(t.sum g) = t.sum fun i d => g i d :=
  rfl

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