trace_add

Mathlib.LinearAlgebra.Matrix.Trace

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

English

The trace is additive over sums: tr(A+B) = tr(A) + tr(B).

Русский

След линейно суммируется: tr(A+B) = tr(A) + tr(B).

LaTeX

$$$$ \operatorname{tr}(A + B) = \operatorname{tr}(A) + \operatorname{tr}(B) $$$$

Lean4

@[simp]
theorem trace_add (A B : Matrix n n R) : trace (A + B) = trace A + trace B :=
  Finset.sum_add_distrib

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

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

Разделы

Аффилиация

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