English
If the two indices differ in their second component (k ≠ k'), then blockDiagonal M at those indices is zero.
Русский
Если два индекса различаются по второй составной части (k ≠ k'), блочная диагональ применяется к этим индексам и даёт ноль.
LaTeX
$$$\text{If } k \neq k',\quad \operatorname{blockDiagonal} M\langle i,k\rangle \langle j,k'\rangle = 0.$$$
Lean4
theorem blockDiagonal_apply_ne (M : o → Matrix m n α) (i j) {k k'} (h : k ≠ k') : blockDiagonal M (i, k) (j, k') = 0 :=
if_neg h