proposition: Lemma rank_I n : \rank (1%:M : 'M[F]_n) = n.
proof: Proof. apply/eqP. apply/row_freeP. exists (1%:M : 'M[F]_n); by rewrite mulmx1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2