proposition: Lemma scalar_mx_comm : forall (n : pos_nat) a (A : matrix R n n), A *m (a%:M) === (a%:M) *m A.
proof: Proof. move=> n a A; apply: trmx_inj; rewrite -> trmx_mul, trmx_scalar. by rewrite -> !mulmx_scalar, trmx_scale; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms