proposition: Lemma scalemx0 : forall x, x *m: '0m === '0m.
proof: Proof. by rewrite/null_mx/addmx/oppmx/scalemx=> x i j; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms