proposition: Lemma mx_trace_tr : forall n (A : 'M_n), \tr A^T === \tr A.
proof: Proof. by move=> n A; apply eq_bigr=> i _; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms