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(A(BC)) = tr(C(AB)).

Русский

Для A,B,C: tr(A(BC)) = tr(C(AB)).

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 [← Matrix.mul_assoc, trace_mul_comm]

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

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

Разделы

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

Аффилиация

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