finsupp_sum_apply — Mathlib

English

Evaluating the finsupp sum of linear maps at a vector b equals the sum of the evaluations of the individual maps at b.

Русский

Оценка суммы по FinSupp линейных отображений на векторе b равна сумме оценок отдельных отображений на b.

LaTeX

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

Lean4

@[simp]
theorem finsupp_sum_apply (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M) : (t.sum g) b = t.sum fun i d => g i d b :=
  sum_apply _ _ _

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