proposition: Lemma mulmx_scalar : forall m n a (A : 'M_(m, n)), (a%:M) *m A === a *m: A.
proof: Proof. move=> m n a A i j; rewrite/block_mx/pastemx/trmx/null_mx/addmx/oppmx/scalemx/scalar_mx/mulmx. setoid_rewrite (bigD1 (j:=i))=>//. setoid_rewrite big1=>[|i'/=]; first by case: eqP=>ii'//; ring. by rewrite/is_true eq_sym; move/negbRL=>->/=; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms