toBlock_one_self — Mathlib

English

For any block decomposition, the diagonal block corresponding to a single block is the identity on that block.

Русский

Для любого разбиения на блоки диагональный блок, соответствующий одному блоку, является единичной матрицей на этом блоке.

LaTeX

$$$\operatorname{toBlock}\bigl(1: Matrix\, m\, m\, \alpha\bigr)\; p\; p = 1.$$$

Lean4

@[simp]
theorem toBlock_one_self (p : m → Prop) : Matrix.toBlock (1 : Matrix m m α) p p = 1 :=
  toBlock_diagonal_self _ p

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