blockDiag_blockDiagonal — Mathlib

English

Block diagonalization at the level of a family M gives back the original family when composed with blockDiagonal.

Русский

Блочная диагонализация блока возвращает исходную семью матриц при композиции с blockDiagonal.

LaTeX

$$$ blockDiag (blockDiagonal M) = M $$$

Lean4

@[simp]
theorem blockDiag_blockDiagonal [DecidableEq o] (M : o → Matrix m n α) : blockDiag (blockDiagonal M) = M :=
  funext fun _ => ext fun i j => blockDiagonal_apply_eq M i j _

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