trace_mul_comm

Mathlib.LinearAlgebra.Matrix.Trace

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

← MathLib Explorer

English

For square matrices, tr(AB) = tr(BA).

Русский

Для квадратных матриц: tr(AB) = tr(BA).

LaTeX

$$$$ \operatorname{tr}(AB) = \operatorname{tr}(BA) $$$$

Lean4

theorem trace_mul_comm [AddCommMonoid R] [CommMagma R] (A : Matrix m n R) (B : Matrix n m R) :
    trace (A * B) = trace (B * A) := by rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]

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

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

Разделы

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

Аффилиация

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