IsTwoBlockDiagonal — Mathlib

English

A 2x2 block matrix is block diagonal precisely when the off-diagonal blocks vanish, i.e., the upper-right and lower-left blocks are zero.

Русский

2x2 блочная матрица является блочно диагональной тогда и только тогда, когда вне диагонали блоки равны нулю (верхний правый и нижний левый блоки нули).

LaTeX

$$$ \\text{IsTwoBlockDiagonal}(A) \\;\\equiv\\; \\text{toBlocks}_{12} A = 0 \\;\\land\\; \\text{toBlocks}_{21} A = 0 $$$

Lean4

/-- A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish -/
def IsTwoBlockDiagonal [Zero α] (A : Matrix (n ⊕ o) (l ⊕ m) α) : Prop :=
  toBlocks₁₂ A = 0 ∧ toBlocks₂₁ A = 0

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