proposition: Lemma tens_scalar1mx (m n : nat) (M : 'M_(m,n)) : 1 *t M = castmx (esym (mul1n _), esym (mul1n _)) M.
proof: Proof. by rewrite tens_scalar_mx scale1r. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)