proposition: Lemma tensmx_decl : forall (R : comRingType) m n (M :'M[R]_m) (N : 'M[R]_n), M *t N = (1%:M *t N) *m (M *t 1%:M).
proof: Proof. by move=> R0 m n M N; rewrite tensmx_mul mul1mx mulmx1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)