toBlocks₁₂_diagonal — Mathlib

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

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