trace_sub

Mathlib.LinearAlgebra.Matrix.Trace

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

English

For any matrices A,B, tr(A - B) = tr(A) - tr(B).

Русский

Для любых матриц A,B: tr(A - B) = tr(A) - tr(B).

LaTeX

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

Lean4

@[simp]
theorem trace_sub (A B : Matrix n n R) : trace (A - B) = trace A - trace B :=
  Finset.sum_sub_distrib ..

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

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

Разделы

Аффилиация

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