proposition: Lemma mx_trace_scale : forall n a (A : 'M_n), \tr (a *m: A) === a * \tr A.
proof: Proof. by move=> n a A; rewrite/mx_trace; setoid_rewrite (big_distrr (I:=ordinal_finType n)); 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