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