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 bottom-left block in the 2×2 block decomposition is the zero matrix.

Русский

Пусть l и m — множества индексов; для диагональной матрицы diag(v) с v: l ⊕ m → α в разбиении на 2×2 блоки нижний левый блок равен нулю.

LaTeX

$$$\operatorname{toBlocks}_{21}\bigl(\operatorname{diagonal}(v)\bigr) = 0.$$$

Lean4

@[simp]
theorem toBlocks₂₁_diagonal (v : l ⊕ m → α) : toBlocks₂₁ (diagonal v) = 0 :=
  rfl

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