matrix_diagonal — Mathlib

English

If HasSum f a, then HasSum (fun x => diagonal (f x)) (diagonal a).

Русский

Если имеет место сумма HasSum f a, то сумма диагоналей также имеет форму diagonal(a).

LaTeX

$$$\\operatorname{HasSum}(f,a,L) \\Rightarrow \\operatorname{HasSum}(x \\mapsto \\operatorname{diagonal}(f(x)), \\operatorname{diagonal}(a), L)$$$

Lean4

theorem matrix_diagonal [DecidableEq n] {f : X → n → R} {a : n → R} (hf : HasSum f a L) :
    HasSum (fun x => diagonal (f x)) (diagonal a) L :=
  hf.map (diagonalAddMonoidHom n R) continuous_id.matrix_diagonal

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