blockDiagonal'_eq_blockDiagonal

Mathlib.Data.Matrix.Block

URI: https://scilib.ai/kg/mathlib#Matrix.blockDiagonal'_eq_blockDiagonal

← MathLib Explorer

English

The submatrix of blockDiagonal' equals blockDiagonal.

Русский

Подматрица blockDiagonal' равна blockDiagonal.

LaTeX

$$$ (blockDiagonal' M).submatrix (Prod.toSigma \circ Prod.swap) (Prod.toSigma \circ Prod.swap) = blockDiagonal M $$$

Lean4

theorem blockDiagonal'_eq_blockDiagonal (M : o → Matrix m n α) {k k'} (i j) :
    blockDiagonal M (i, k) (j, k') = blockDiagonal' M ⟨k, i⟩ ⟨k', j⟩ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru