blockDiagonal_one — Mathlib

English

If m is the index type and the ring α has 1, then blockDiagonal of the constant identity blocks is the identity.

Русский

Если размерность блочной диагонали равна m и над тёзм α имеется единица, то блочная диагональ единичных блоков равна единице.

LaTeX

$$$\operatorname{blockDiagonal}(1) = 1.$$$

Lean4

@[simp]
theorem blockDiagonal_one [DecidableEq m] [One α] : blockDiagonal (1 : o → Matrix m m α) = 1 :=
  show (blockDiagonal fun _ : o => diagonal fun _ : m => (1 : α)) = diagonal fun _ => 1 by rw [blockDiagonal_diagonal]

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