matrix_blockDiag — Mathlib

English

If f sums to a, then the blockDiag of f sums to the blockDiag of a.

Русский

Если f суммируется к a, то blockDiag(f) суммируется к blockDiag(a).

LaTeX

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

Lean4

theorem matrix_blockDiag {f : X → Matrix (m × p) (n × p) R} {a : Matrix (m × p) (n × p) R} (hf : HasSum f a L) :
    HasSum (fun x => blockDiag (f x)) (blockDiag a) L :=
  (hf.map (blockDiagAddMonoidHom m n p R) <| Continuous.matrix_blockDiag continuous_id :)

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