coe_sum' — Mathlib

English

The sum of endomorphisms, viewed as linear maps, satisfies that the sum in the endomorphism space corresponds to the sum of their linear map representations.

Русский

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

LaTeX

$$$\\text{sum of endomorphisms corresponds to sum of their linear maps, i.e. } (f+g)^{\\text{lin}} = f^{\\text{lin}} + g^{\\text{lin}}.$$$

Lean4

@[simp, norm_cast]
theorem coe_sum' {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) : ⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d) := by
  simp only [← coe_coe, coe_sum, LinearMap.coeFn_sum]

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