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