Matrix.trace_mul_comm

theorem Matrix.trace_mul_comm : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : AddCommMonoid R] [inst_3 : CommSemigroup R] (A : Matrix m n R) (B : Matrix n m R), (A * B).trace = (B * A).trace

This theorem states that for any types `m` and `n`, and a type `R` with structures of a finite type, an addition-commutative monoid and a commutative semigroup, given two matrices `A` and `B` of types `Matrix m n R` and `Matrix n m R` respectively, the trace of the product `A * B` is equal to the trace of the product `B * A`. In other words, the trace of the product of two matrices is commutative. This mirrors the familiar property from linear algebra where the trace of the product of two matrices is invariant under cyclic permutations.

More concisely: For any types `m`, `n`, and matrices `A` of size `m x n` and `B` of size `n x m` over a commutative semigroup `R` with finite type and additive commutativity, the trace of their product `A * B` equals the trace of `B * A`.