blockDiagonal_apply — Mathlib

English

In the blockDiagonal decomposition, the block at (i,k) and (j,k) equals M(k)_{i,j}.

Русский

В разложении на блоки блочная величина в позиции (i,k), (j,k) равна M(k)_{i j}.

LaTeX

$$$\operatorname{blockDiagonal} M\{ fst := i, snd := k \}\{ fst := j, snd := k \} = M(k)_{i j}$$$

Lean4

theorem blockDiagonal_apply (M : o → Matrix m n α) (ik jk) :
    blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0 :=
  rfl

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