proposition: Lemma full_rank_inj m n (A : 'M[F]_(m, n)) : m <= n -> \rank A = m -> forall (a b : 'rV[F]_m), a *m A = b *m A -> a = b.
proof: Proof. move=> Hmn Hrank a b Hab. move: Hrank. rewrite /mxrank. destruct m => //= [_|]. by rewrite (empty_rV a) (empty_rV b). destruct n => //=. unlock. move Herk : (Gaussian_elimination A) => LUr /= Htmp. move: (mulmx_ebase A) => Heq. rewrite -Heq !mulmxA in Hab. have {}Hab : a *m col_ebase A *m pid_mx (\rank A) *m row_ebase A *m (invmx (row_ebase A)) = b *m col_ebase A *m pid_mx (\rank A) *m row_ebase A *m (invmx (row_ebase A)). by rewrite Hab. rewrite -!mulmxA mulmxV in Hab; last by exact: row_ebase_unit. rewrite mulmx1 !mulmxA /mxrank /= in Hab. unlock in Hab. rewrite !Htmp in Hab. move: {Heq}(@pid_mx_inj _ _ _ (a *m col_ebase A) (b *m col_ebase A) Hmn Hab) => Heq. have {}Hab : a *m col_ebase A *m (invmx (col_ebase A)) = b *m col_ebase A *m (invmx (col_ebase A)) by rewrite Heq. rewrite -!mulmxA mulmxV in Hab; last by apply: col_ebase_unit. by rewrite !mulmx1 in Hab. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2