proposition: Lemma card_GL n : n > 0 -> #|'GL_n[F]| = (#|F| ^ 'C(n, 2) * \prod_(1 <= i < n.+1) (#|F| ^ i - 1))%N.
proof: Proof. case: n => // n' _; set n := n'.+1; set p := #|F|. rewrite big_nat_rev big_add1 -triangular_sum expn_sum -big_split /=. pose fr m := [pred A : 'M[F]_(m, n) | \rank A == m]. set m := n; rewrite [in m.+1]/m; transitivity #|fr m|. by rewrite cardsT /= card_sub; apply: eq_card => A; rewrite -row_free_unit. have: m <= n by []; elim: m => [_ | m IHm /ltnW-le_mn]. rewrite (@eq_card1 _ (0 : 'M_(0, n))) ?big_geq //= => A. by rewrite flatmx0 !inE mxrank.unlock !eqxx. rewrite big_nat_recr // -{}IHm //= !subSS mulnBr muln1 -expnD subnKC //. rewrite -sum_nat_const /= -sum1_card -add1n. rewrite (partition_big dsubmx (fr m)) /= => [|A]; last first. rewrite !inE -{1}(vsubmxK A); move: {A}(_ A) (_ A) => Ad Au Afull. rewrite eqn_leq rank_leq_row -(leq_add2l (\rank Au)) -mxrank_sum_cap. rewrite {1 3}[@mxrank]lock addsmxE (eqnP Afull) -lock -addnA. by rewrite leq_add ?rank_leq_row ?leq_addr. apply: eq_bigr => A rAm; rewrite (reindex (col_mx^~ A)) /=; last first. exists usubmx => [v _ | vA]; first by rewrite col_mxKu. by case/andP=> _ /eqP <-; rewrite vsubmxK. transitivity #|~: [set v *m A | v in 'rV_m]|; last first. rewrite cardsCs setCK card_imset ?card_mx ?card_ord ?mul1n //. have [B AB1] := row_freeP rAm; apply: can_inj (mulmx^~ B) _ => v. by rewrite -mulmxA AB1 mulmx1. rewrite -sum1_card; apply: eq_bigl => v; rewrite !inE col_mxKd eqxx. rewrite andbT eqn_leq rank_leq_row /= -(leq_add2r (\rank (v :&: A)%MS)). rewrite -addsmxE mxrank_sum_cap (eqnP rAm) addnAC leq_add2r. rewrite (ltn_leqif (mxrank_leqif_sup _)) ?capmxSl // sub_capmx submx_refl. by congr (~~ _); apply/submxP/imsetP=> [] [u]; exists u. 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 finalg zmodp matrix)