proposition: Proposition proj_eigenspace_cycle_sub_quasi_cent i j : ('E_(i, i + j) <= 'E_j)%MS.
proof: Proof. apply/(@memmx_subP F _ _ q)=> A /E2iP[ViA Vi'A]. apply/EiP; apply: canLR (mulKmx inj_g) _; rewrite -{1}[A]mul1mx -{2}[g]mul1mx. have: (1%:M <= sumV)%MS by have [->] := mxdirect_sum_eigenspace_cycle. case/sub_sumsmxP=> p ->; rewrite -!mulmxA !mulmx_suml. apply: eq_bigr=> k _; have [-> | ne_ki] := eqVneq (k : nat) (i %% h)%N. rewrite Vi_mod -mulmxA (mulmxA _ A) (eigenspaceP ViA). rewrite (mulmxA _ g) (eigenspaceP (submxMl _ _)). by rewrite -!(scalemxAl, scalemxAr) scalerA mulmxA exprD. rewrite 2!mulmxA (eigenspaceP (submxMl _ _)) -!(scalemxAr, scalemxAl). by rewrite -(mulmxA _ 'V_k A) Vi'A ?linear0 ?mul0mx ?scaler0 // 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)