blockDiagonal_apply_ne — Mathlib

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

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