blockDiagonal_add — Mathlib

English

BlockDiagonal distributes over addition: blockDiagonal(M + N) = blockDiagonal(M) + blockDiagonal(N).

Русский

Блочная диагональ распределяется по сложению: blockDiagonal(M + N) = blockDiagonal(M) + blockDiagonal(N).

LaTeX

$$$\operatorname{blockDiagonal}(M+N) = \operatorname{blockDiagonal}(M) + \operatorname{blockDiagonal}(N).$$$

Lean4

@[simp]
theorem blockDiagonal_add [AddZeroClass α] (M N : o → Matrix m n α) :
    blockDiagonal (M + N) = blockDiagonal M + blockDiagonal N :=
  by
  ext
  simp only [blockDiagonal_apply, Pi.add_apply, add_apply]
  split_ifs <;> simp

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