proposition: Lemma rank_abs_irr_dvd_solvable F gT (G : {group gT}) n rG : @mx_absolutely_irreducible F _ G n rG -> solvable G -> n %| #|G|.
proof: Proof. move=> absG solG. without loss closF: F rG absG / group_closure_field F gT. move=> IH; apply: (@group_closure_field_exists gT F) => [[F' f closF']]. by apply: IH (map_repr f rG) _ closF'; rewrite map_mx_abs_irr. elim: {G}_.+1 {-2}G (ltnSn #|G|) => // m IHm G leGm in n rG absG solG *. have [G1 | ntG] := eqsVneq G 1%g. by rewrite abelian_abs_irr ?G1 ?abelian1 // in absG; rewrite (eqP absG) dvd1n. have [H nsHG p_pr] := sol_prime_factor_exists solG ntG. set p := #|G : H| in p_pr. pose sHG := normal_sub nsHG; pose rH := subg_repr rG sHG. have irrG := mx_abs_irrW absG. wlog [L simL _]: / exists2 L, mxsimple rH L & (L <= 1%:M)%MS. by apply: mxsimple_exists; rewrite ?mxmodule1 //; case: irrG. have ltHG: H \proper G. by rewrite properEcard sHG -(Lagrange sHG) ltn_Pmulr // prime_gt1. have dvLH: \rank L %| #|H|. have absL: mx_absolutely_irreducible (submod_repr (mxsimple_module simL)). exact/closF/submod_mx_irr. apply: IHm absL (solvableS (normal_sub nsHG) solG). by rewrite (leq_trans (proper_card ltHG)). have [_ [x Gx H'x]] := properP ltHG. have prGH: prime #|G / H|%g by rewrite card_quotient ?normal_norm. wlog sH: / socleType rH by apply: socle_exists. pose W := PackSocle (component_socle sH simL). have card_sH: #|sH| = #|G : 'C_G[W | 'Cl]|. rewrite -cardsT; have ->: setT = orbit 'Cl G W. apply/eqP; rewrite eqEsubset subsetT. have /imsetP[W' _ defW'] := Clifford_atrans irrG sH. have WW': W' \in orbit 'Cl G W by rewrite orbit_in_sym // -defW' inE. by rewrite defW' andbT; apply/subsetP=> W'' /orbit_in_trans->. rewrite orbit_stabilizer // card_in_imset //. exact: can_in_inj (act_reprK _). have sHcW: H \subset 'C_G[W | 'Cl]. apply: subset_trans (subset_trans (joing_subl _ _) (Clifford_astab sH)) _. by rewrite subsetI subsetIl astabS ?subsetT. have [|] := prime_subgroupVti ('C_G[W | 'Cl] / H)%G prGH. rewrite quotientSGK ?normal_norm // => cClG. have def_sH: setT = [set W]. apply/eqP; rewrite eq_sym eqEcard subsetT cards1 cardsT card_sH. by rewrite -indexgI (setIidPl cClG) indexgg. suffices L1: (L :=: 1%:M)%MS. by rewrite L1 mxrank1 in dvLH; apply: dvdn_trans (cardSg sHG). apply/eqmxP; rewrite submx1. have cycH: cyclic (G / H)%g by rewrite prime_cyclic. have [y Gy|_ _] := mx_irr_prime_index closF irrG cycH simL; last first. by apply; rewrite ?submx1 //; case simL. have simLy: mxsimple rH (L *m rG y) by apply: Clifford_simple. pose Wy := PackSocle (component_socle sH simLy). have: (L *m rG y <= Wy)%MS by rewrite PackSocleK component_mx_id. have ->: Wy = W by apply/set1P; rewrite -def_sH inE. by rewrite PackSocleK; apply: component_mx_iso. rewrite (setIidPl _) ?quotientS ?subsetIl // => /trivgP. rewrite quotient_sub1 //; last by rewrite subIset // normal_norm. move/setIidPl; rewrite (setIidPr sHcW) /= => defH. rewrite -(Lagrange sHG) -(Clifford_rank_components irrG W) card_sH -defH. rewrite mulnC dvdn_pmul2r // (_ : W :=: L)%MS //; apply/eqmxP. have sLW: (L <= W)%MS by rewrite PackSocleK component_mx_id. rewrite andbC sLW; have [modL nzL _] := simL. have [_ _] := (Clifford_rstabs_simple irrG W); apply=> //. rewrite /mxmodule rstabs_subg /= -Clifford_astab1 -astabIdom -defH. by rewrite -(rstabs_subg rG sHG). 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)