proposition: Lemma mulmxP (K : fieldType) (m n : nat) (A B : 'M[K]_(m, n)) : reflect (forall u : 'rV__, u *m A = u *m B) (A == B).
proof: Proof. apply: (iffP eqP) => [-> //|eqAB]. apply: (@row_full_inj _ _ _ _ 1%:M); first by rewrite row_full_unit unitmx1. by apply/row_matrixP => i; rewrite !row_mul eqAB. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)