diag_list_sum

Mathlib.Data.Matrix.Basic

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

English

For any list of matrices, the diagonal of the sum equals the sum of the diagonals.

Русский

Для любого списка матриц диагональ суммы равна сумме диагоналей.

LaTeX

$$$\\operatorname{diag}\\left(\\sum l\\right) = \\sum \\operatorname{diag}(l)$$$

Lean4

@[simp]
theorem diag_list_sum [AddMonoid α] (l : List (Matrix n n α)) : diag l.sum = (l.map diag).sum :=
  map_list_sum (diagAddMonoidHom n α) l

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

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

Разделы

Аффилиация

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