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