blockDiag_apply

Mathlib.Data.Matrix.Block

URI: https://scilib.ai/kg/mathlib#Matrix.blockDiag_apply

English

For any M, k, i, j, the (i, j)-entry of blockDiag M k equals M (i, k) (j, k).

Русский

Для любых M, k, i, j, элемент на позиции (i, j) в blockDiag M k равен M (i, k) (j, k).

LaTeX

$$$ (blockDiag M k)_{i j} = M_{(i,k),(j,k)} $$$

Lean4

theorem blockDiag_apply (M : Matrix (m × o) (n × o) α) (k : o) (i j) : blockDiag M k i j = M (i, k) (j, k) :=
  rfl

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

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

Разделы

Аффилиация

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