proposition: Lemma mx_trace_scalar : forall n a, \tr (a%:M : 'M_n) === a *+ n.
proof: Proof. by move=> n a; rewrite <- big_const_ord; apply eq_bigr=> i _; rewrite/scalar_mx eq_refl; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms