trace_mul_cycle

Mathlib.LinearAlgebra.Matrix.Trace

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

← MathLib Explorer

English

For A,B,C, tr(ABC) = tr(CAB).

Русский

Для матриц A,B,C: tr(ABC) = tr(CAB).

LaTeX

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

Lean4

theorem trace_mul_cycle [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) :
    trace (A * B * C) = trace (C * A * B) := by rw [trace_mul_comm, Matrix.mul_assoc]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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