proposition: Lemma tuple_of_row_inj n : injective (@tuple_of_row n).
proof: Proof. move=> i j ij. apply/rowP => m0. move/(congr1 (fun x => x !_ m0)) : ij. by rewrite 2!tnth_mktuple. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2