proposition: Lemma LUP_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 cardsT /= card_sub /GRing.unit /= big_add1 /= -triangular_sum -/n /=. elim: {n'}n => [|n IHn]. rewrite !big_geq // mul1n (@eq_card _ _ predT) ?card_mx //= => M. by rewrite {1}[M]flatmx0 -(flatmx0 1%:M) unitmx1. rewrite !big_nat_recr //= expnD mulnAC mulnA -{}IHn -mulnA mulnC. set LHS := #|_|; rewrite -[n.+1]muln1 -{2}[n]mul1n {}/LHS. rewrite -!card_mx subn1 -(cardC1 0) -mulnA; set nzC := predC1 _. rewrite -sum1_card (partition_big lsubmx nzC) => [|A]; last first. rewrite unitmxE unitfE; apply: contra; move/eqP=> v0. rewrite -[A]hsubmxK v0 -[n.+1]/(1 + n)%N -col_mx0. rewrite -[rsubmx _]vsubmxK -det_tr tr_row_mx !tr_col_mx !trmx0. by rewrite det_lblock [0]mx11_scalar det_scalar1 mxE mul0r. rewrite -sum_nat_const; apply: eq_bigr => /= v /cV0Pn[k nza]. have xrkK: involutive (@xrow F _ _ 0 k). by move=> m A /=; rewrite /xrow -row_permM tperm2 row_perm1. rewrite (reindex_inj (inv_inj (xrkK (1 + n)%N))) /= -[n.+1]/(1 + n)%N. rewrite (partition_big ursubmx xpredT) //= -sum_nat_const. apply: eq_bigr => u _; set a : F := v _ _ in nza. set v1 : 'cV_(1 + n) := xrow 0 k v. have def_a: usubmx v1 = a%:M. by rewrite [_ v1]mx11_scalar mxE lshift0 mxE tpermL. pose Schur := dsubmx v1 *m (a^-1 *: u). pose L : 'M_(1 + n) := block_mx a%:M 0 (dsubmx v1) 1%:M. pose U B : 'M_(1 + n) := block_mx 1 (a^-1 *: u) 0 B. rewrite (reindex (fun B => L *m U B)); last first. exists (fun A1 => drsubmx A1 - Schur) => [B _ | A1]. by rewrite mulmx_block block_mxKdr mul1mx addrC addKr. rewrite !inE mulmx_block !mulmx0 mul0mx !mulmx1 !addr0 mul1mx addrC subrK. rewrite mul_scalar_mx scalerA divff // scale1r andbC; case/and3P => /eqP <- _. rewrite -{1}(hsubmxK A1) xrowE mul_mx_row row_mxKl -xrowE => /eqP def_v. rewrite -def_a block_mxEh vsubmxK /v1 -def_v xrkK. apply: trmx_inj; rewrite tr_row_mx tr_col_mx trmx_ursub trmx_drsub trmx_lsub. by rewrite hsubmxK vsubmxK. rewrite -sum1_card; apply: eq_bigl => B; rewrite xrowE unitmxE. rewrite !det_mulmx unitrM -unitmxE unitmx_perm det_lblock det_ublock. rewrite !det_scalar1 det1 mulr1 mul1r unitrM unitfE nza -unitmxE. rewrite mulmx_block !mulmx0 mul0mx !addr0 !mulmx1 mul1mx block_mxKur. rewrite mul_scalar_mx scalerA divff // scale1r eqxx andbT. by rewrite block_mxEh mul_mx_row row_mxKl -def_a vsubmxK -xrowE xrkK eqxx andbT. 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)