proposition: Lemma scalemx_inj m n a : a != 0 -> injective ( *:%R a : 'M[R]_(m, n) -> 'M[R]_(m, n)).
proof: Proof. move=> nz_a A B eq_aAB; apply: contraNeq nz_a. rewrite -[A == B]subr_eq0 -[a == 0]orbF => /negPf<-. by rewrite -scalemx_eq0 linearB subr_eq0 /= eq_aAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)