sum_comp_single — Mathlib

English

Another instance of evaluation for Pi.compRightL: for all α, i, the equality (Pi.compRightL f) v evaluated at i equals v(f(i)).

Русский

Ещё одно свойство оценки Pi.compRightL: для всех α и i верно (Pi.compRightL f) v при i равно v(f(i)).

LaTeX

$$$$ (\Pi.compRightL\; f\; v)(i) = v(f(i)) $$$$

Lean4

theorem sum_comp_single [Fintype ι] [DecidableEq ι] (L : (Π i, φ i) →L[R] M) (v : Π i, φ i) :
    ∑ i, L.comp (.single R φ i) (v i) = L v := by simp [← map_sum, LinearMap.sum_single_apply]

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