Trace Cyclic Property

Statement

For any $m \times n$ matrix $A$ and $n \times m$ matrix $B$ over a commutative ring $R$:

More generally, the trace is invariant under cyclic permutations of a product:

Note that $\operatorname{tr}(ABC) = \operatorname{tr}(BCA) = \operatorname{tr}(CAB)$ in general, but $\operatorname{tr}(ABC) \ne \operatorname{tr}(BAC)$ — only cyclic permutations preserve the trace, not arbitrary ones.

Visualization

Take $A = \begin{pmatrix} 1 & 2 \\ 3 & 4 \end{pmatrix}$ and $B = \begin{pmatrix} 5 & 6 \\ 7 & 8 \end{pmatrix}$.

Compute $AB$:

Compute $BA$:

Product	Matrix	Trace
$AB$	$\begin{pmatrix} 19 & 22 \\ 43 & 50 \end{pmatrix}$	$19 + 50 = 69$
$BA$	$\begin{pmatrix} 23 & 34 \\ 31 & 46 \end{pmatrix}$	$23 + 46 = 69$

Both traces equal $69$, confirming $\operatorname{tr}(AB) = \operatorname{tr}(BA)$.

Proof Sketch

1. Expand by definition. $\operatorname{tr}(AB) = \sum_i (AB)_{ii} = \sum_i \sum_j A_{ij} B_{ji}$.
2. Swap summation. $\sum_i \sum_j A_{ij} B_{ji} = \sum_j \sum_i B_{ji} A_{ij} = \sum_j (BA)_{jj} = \operatorname{tr}(BA)$.
3. Commutativity of $R$. The interchange $A_{ij} B_{ji} = B_{ji} A_{ij}$ uses that $R$ is commutative.
4. Cyclic extension. $\operatorname{tr}(ABC) = \operatorname{tr}((AB)C) = \operatorname{tr}(C(AB)) = \operatorname{tr}(CAB)$; apply inductively.

Connections

• Cayley–Hamilton TheoremCayley–Hamilton Theorem$$p_A(A) = 0 \;\text{where}\; p_A(\lambda) = \det(\lambda I - A)$$Every square matrix satisfies its own characteristic polynomialRead more → — the proof of Cayley–Hamilton for matrices over a commutative ring uses the trace (and more generally the symmetric functions of eigenvalues) to identify coefficients of the characteristic polynomial
• Determinant MultiplicativityDeterminant Multiplicativity$$\det(AB) = \det(A)\,\det(B)$$The determinant of a product equals the product of determinantsRead more → — both trace and determinant are similarity invariants; $\operatorname{tr}(PAP^{-1}) = \operatorname{tr}(A)$ follows from the cyclic property applied to $P$, $A$, $P^{-1}$
• Sylvester Determinant TheoremSylvester Determinant Theorem$$\det(I_m + AB) = \det(I_n + BA)$$det(Im + AB) = det(In + BA) for any m×n matrix A and n×m matrix B.Read more → — a determinant analogue: just as $\det(I+AB) = \det(I+BA)$, the cyclic property gives $\operatorname{tr}(AB) = \operatorname{tr}(BA)$ as a first-order version of the same symmetry

import Mathlib.LinearAlgebra.Matrix.Trace

/-- Trace cyclic property: tr(A * B) = tr(B * A).
    Mathlib's direct alias is `Matrix.trace_mul_comm`. -/
theorem trace_cyclic
    {R : Type*} [AddCommMonoid R] [CommMagma R]
    {m n : Type*} [Fintype m] [Fintype n]
    (A : Matrix m n R) (B : Matrix n m R) :
    Matrix.trace (A * B) = Matrix.trace (B * A) :=
  Matrix.trace_mul_comm A B