blockDiag_add

Mathlib.Data.Matrix.Block

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

English

BlockDiag distributes over addition.

Русский

blockDiag распределяет по сложению.

LaTeX

$$$ blockDiag (M + N) = blockDiag M + blockDiag N $$$

Lean4

@[simp]
theorem blockDiag_add [Add α] (M N : Matrix (m × o) (n × o) α) : blockDiag (M + N) = blockDiag M + blockDiag N :=
  rfl

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

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

Разделы

Аффилиация

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