English
Let l and m be index sets and α a type. For any diagonal matrix diag(v) with v: l ⊕ m → α, the top-right block in the 2×2 block decomposition is the zero matrix.
Русский
Пусть l и m — множества индексов; для диагональной матрицы diag(v) с v: l ⊕ m → α в разбиении на 2×2 блоки верхний правый блок равен нулю.
LaTeX
$$$\operatorname{toBlocks}_{12}\bigl(\operatorname{diagonal}(v)\bigr) = 0.$$$
Lean4
@[simp]
theorem toBlocks₁₂_diagonal (v : l ⊕ m → α) : toBlocks₁₂ (diagonal v) = 0 :=
rfl