coe_sum — Mathlib

English

The underlying function of the sum of two endomorphisms equals the sum of their underlying functions: (f+g) = f+g as functions.

Русский

Основная функция суммы эндоморфизмов равна сумме их функций: (f+g) = f+g как функции.

LaTeX

$$$\\uparrow(f+g) = \\uparrow f + \\uparrow g$ as functions.$$

Lean4

@[simp, norm_cast]
theorem coe_sum {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
    ↑(∑ d ∈ t, f d) = (∑ d ∈ t, f d : M₁ →ₛₗ[σ₁₂] M₂) :=
  map_sum (AddMonoidHom.mk ⟨((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂), rfl⟩ fun _ _ => rfl) _ _

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