trace_multiset_sum

Mathlib.LinearAlgebra.Matrix.Trace

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

English

For a multiset s of matrices, tr(s.sum) = (map trace s).sum.

Русский

Для мультисета s матриц, след равен сумме следов элементов мультисета.

LaTeX

$$$$ \operatorname{tr}\left( \sum s \right) = \sum \operatorname{tr}(\cdot) \, s $$$$

Lean4

@[simp]
theorem trace_multiset_sum (s : Multiset (Matrix n n R)) : trace s.sum = (s.map trace).sum :=
  map_multiset_sum (traceAddMonoidHom n R) s

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

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

Разделы

Аффилиация

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