blockDiagonal_apply' — Mathlib

English

For a family of matrices M, a point (i, k) and (j, k'), the blockDiagonal M evaluated at these indices equals M(k)_{i,j} if k = k', otherwise 0.

Русский

Для семейства матриц M, точка (i,k) и (j,k') дают значение блока blockDiagonal(M) равное M(k)_{i,j} если k=k', иначе 0.

LaTeX

$$$\operatorname{blockDiagonal} M\langle i,k\rangle\langle j,k'\rangle = \begin{cases} M(k)_{i j}, & \text{если } k = k'\\ 0, & \text{иначе} \end{cases}$$$

Lean4

theorem blockDiagonal_apply' (M : o → Matrix m n α) (i k j k') :
    blockDiagonal M ⟨i, k⟩ ⟨j, k'⟩ = if k = k' then M k i j else 0 :=
  rfl

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