diagonal_tsum — Mathlib

English

Let f : X → n → R be a function. Then the diagonal of the total sum equals the sum of the diagonals: diag( tsum_L f ) = tsum_L ( diag(f) ).

Русский

Пусть f : X → n → R. Тогда диагональ от суммирования равна сумме диагоналей: diag(tsum_L f) = tsum_L diag(f).

LaTeX

$$$\operatorname{diag}\left(\operatorname{tsum}(f,L)\right) = \operatorname{tsum}\left(\operatorname{diag}(f)\right)(L)$$$

Lean4

theorem diagonal_tsum [DecidableEq n] [T2Space R] {f : X → n → R} : diagonal (∑'[L] x, f x) = ∑'[L] x, diagonal (f x) :=
  Function.LeftInverse.map_tsum f (g := diagonalAddMonoidHom n R) continuous_id.matrix_diagonal continuous_matrix_diag
    diag_diagonal

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