proposition: Proposition rank_proj_eigenspace_cycle i t : \rank 'E_(i, t) = ('n_i * 'n_t)%N.
proof: Proof. have [def1V] := mxdirect_sum_eigenspace_cycle; move/mxdirect_sumsP=> dxV. pose p (i : 'I_h) := proj_mx 'V_i (\sum_(j | j != i) 'V_j)%MS. have def1p: 1%:M = \sum_i p i. rewrite -[\sum_i _]mul1mx; move/eqmxP: def1V; rewrite submx1. case/sub_sumsmxP=> u ->; rewrite mulmx_sumr; apply: eq_bigr => j _. rewrite (bigD1 j) //= mulmxDl proj_mx_id ?submxMl ?dxV //. rewrite proj_mx_0 ?dxV ?addr0 ?summx_sub // => k ne_kj. by rewrite (sumsmx_sup k) ?submxMl. move: i t => i0 t0; pose i := inh i0; pose t := inh t0. transitivity (\rank 'E_(i, t)); first by rewrite /E2_ !Vi_mod modn_mod. transitivity ('n_i * 'n_t)%N; last by rewrite /n_ !Vi_mod. move: {i0 t0}i t => i t; pose Bi := row_base 'V_i; pose Bt := row_base 'V_t. pose B := lin_mx (mulmx (p i *m pinvmx Bi) \o mulmxr Bt). pose B' := lin_mx (mulmx Bi \o mulmxr (pinvmx Bt)). have Bk : B *m B' = 1%:M. have frVpK m (C : 'M[F]_(m, q)) : row_free C -> C *m pinvmx C = 1%:M. by move/row_free_inj; apply; rewrite mul1mx mulmxKpV. apply/row_matrixP=> k; rewrite row_mul mul_rV_lin /= rowE mx_rV_lin /= -row1. rewrite (mulmxA _ _ Bt) -(mulmxA _ Bt) [Bt *m _]frVpK ?row_base_free //. rewrite mulmx1 2!mulmxA proj_mx_id ?dxV ?eq_row_base //. by rewrite frVpK ?row_base_free // mul1mx vec_mxK. have <-: \rank B = ('n_i * 'n_t)%N by apply/eqP; apply/row_freeP; exists B'. apply/eqP; rewrite eqn_leq !mxrankS //. apply/row_subP=> k; rewrite rowE mul_rV_lin /=. apply/E2iP; split=> [|j ne_ji]. rewrite 3!mulmxA mulmx_sub ?eq_row_base //. rewrite 2!(mulmxA 'V_j) proj_mx_0 ?dxV ?mul0mx //. rewrite (sumsmx_sup (inh j)) ?Vi_mod //. by rewrite (modn_small (valP i)) in ne_ji. apply/(@memmx_subP F _ _ q) => A /E2iP[ViA Vi'A]. apply/submxP; exists (mxvec (Bi *m A *m pinvmx Bt)); rewrite mul_vec_lin /=. rewrite mulmxKpV; last by rewrite eq_row_base (eqmxMr _ (eq_row_base _)). rewrite mulmxA -[p i]mul1mx mulmxKpV ?eq_row_base ?proj_mx_sub // mul1mx. rewrite -{1}[A]mul1mx def1p mulmx_suml (bigD1 i) //= big1 ?addr0 // => j neji. rewrite -[p j]mul1mx -(mulmxKpV (proj_mx_sub _ _ _)) -mulmxA Vi'A ?mulmx0 //. by rewrite !modn_small. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gfunctor commutator gproduct) mathcomp(ssralg finalg zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)