proposition: Lemma tens_scalar_mx (m n : nat) (c : R) (M : 'M_(m,n)): c%:M *t M = castmx (esym (mul1n _), esym (mul1n _)) (c *: M).
proof: Proof. apply/matrixP=> i j. case: (mxtens_indexP i)=> i0 i1; case: (mxtens_indexP j)=> j0 j1. rewrite tensmxE [i0]ord1 [j0]ord1 !castmxE !mxE /= mulr1n. by congr (_ * M _ _); apply: val_inj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)