trace_transpose_mul

Mathlib.LinearAlgebra.Matrix.Trace

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

← MathLib Explorer

English

tr(A^T B^T) = tr(A B).

Русский

tr(A^T B^T) = tr(A B).

LaTeX

$$$$ \operatorname{tr}(A^{\top} B^{\top}) = \operatorname{tr}(A B) $$$$

Lean4

@[simp]
theorem trace_transpose_mul [AddCommMonoid R] [Mul R] (A : Matrix m n R) (B : Matrix n m R) :
    trace (Aᵀ * Bᵀ) = trace (A * B) :=
  Finset.sum_comm

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

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

Разделы

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

Аффилиация

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