proposition: Lemma scalar_mx_add : forall n a b, @scalar_mx n (a + b) === a%:M +m b%:M.
proof: Proof. by move=> n a b i j; rewrite/block_mx/pastemx/trmx/null_mx/addmx/oppmx/scalemx/scalar_mx/mulmx; case: eqP=> _; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms