matrix_diag — Mathlib

English

If a family f: X → n × n R has a HasSum to a (i.e., sums to a matrix a), then the diagonal of f sums to the diagonal of a: diag(f) sums to diag(a).

Русский

Если семейство f: X → n × n R суммируется к матрице a, то диагональ f суммируется к диагонали a.

LaTeX

$$HasSum(f,a,L) ⇒ HasSum((λ x, diag(f x)), diag(a), L)$$

Lean4

theorem matrix_diag {f : X → Matrix n n R} {a : Matrix n n R} (hf : HasSum f a L) :
    HasSum (fun x => diag (f x)) (diag a) L :=
  hf.map (diagAddMonoidHom n R) continuous_matrix_diag

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