sum_apply — Mathlib

English

The sum of a finite family of endomorphisms, when coerced to a sum of linear maps, equals the sum of their coerced maps.

Русский

Сумма конечной семьи эндоморфизмов, приведенная к сумме линейных отображений, равна сумме приведенных отображений.

LaTeX

$$$\\left(\\sum_{d\\in t} f d\\right)^{\\text{lin}} = \\sum_{d\\in t} (f d)^{\\text{lin}}$$$

Lean4

theorem sum_apply {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) (b : M₁) : (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b := by
  simp only [coe_sum', Finset.sum_apply]

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