matrix_blockDiagonal — Mathlib

English

If a family f: X → p → Matrix m×n R sums to a, then the blockDiagonal of f sums to the blockDiagonal of a.

Русский

Если семейство f: X → p → матрицы m×n R суммируется к a, то blockDiagonal(f) суммируется к blockDiagonal(a).

LaTeX

$$HasSum(f,a,L) ⇒ HasSum((λ x, Matrix.blockDiagonal (f x)), Matrix.blockDiagonal a, L)$$

Lean4

theorem matrix_blockDiagonal [DecidableEq p] {f : X → p → Matrix m n R} {a : p → Matrix m n R} (hf : HasSum f a L) :
    HasSum (fun x => blockDiagonal (f x)) (blockDiagonal a) L :=
  hf.map (blockDiagonalAddMonoidHom m n p R) continuous_id.matrix_blockDiagonal

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