sum_apply — Mathlib

English

Evaluating a Finset sum of matrices at a fixed entry commutes with the sum of the entries: (∑ c ∈ s, g c) i j = ∑ c ∈ s, (g c) i j.

Русский

Оценка суммы матриц по фиксированной позиции эквивалентна сумме значений соответствующих позиций.

LaTeX

$$$\\left(\\sum_{c\\in s} g(c)\\right)_{ij} = \\sum_{c\\in s} (g(c))_{ij}$$$

Lean4

theorem sum_apply [AddCommMonoid α] (i : m) (j : n) (s : Finset β) (g : β → Matrix m n α) :
    (∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j :=
  (congr_fun (s.sum_apply i g) j).trans (s.sum_apply j _)

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