proposition: Lemma mx_trace_mulC : forall m n (A : matrix R m n) B, \tr (A *m B) === \tr (B *m A).
proof: Proof. move=> m n A B; transitivity (\sum_(i < m) \sum_(j < n) A i j * B j i). by apply eq_bigr; reflexivity. setoid_rewrite (exchange_big (I:=ordinal_finType m)); apply eq_bigr => i _. by apply eq_bigr => j _; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms