proposition: Lemma mx_rsim_standard : mx_rsim rG standard_grepr.
proof: Proof. pose W i := oapp val 0 (soc i); pose S := (\sum_i W i)%MS. have C'G: [char algC]^'.-group G := algC'G G. have [defS dxS]: (S :=: 1%:M)%MS /\ mxdirect S. rewrite /S mxdirectE /= !(bigID soc xpredT) /=. rewrite addsmxC big1 => [|i]; last by rewrite /W; case (soc i). rewrite adds0mx_id addnC (@big1 nat) ?add0n => [|i]; last first. by rewrite /W; case: (soc i); rewrite ?mxrank0. have <-: Socle sG = 1%:M := reducible_Socle1 sG (mx_Maschke rG C'G). have [W0 _ | noW] := pickP sG; last first. suff no_i: (soc : pred iG) =1 xpred0 by rewrite /Socle !big_pred0 ?mxrank0. by move=> i; rewrite /soc; case: pickP => // W0; have:= noW W0. have irrK Wi: soc (standard_irr Wi) = Some Wi. rewrite /soc; case: pickP => [W' | /(_ Wi)] /= /eqP // eqWi. apply/eqP/socle_rsimP. apply: mx_rsim_trans (rsim_irr_comp iG C'G (socle_irr _)) (mx_rsim_sym _). by rewrite [irr_comp _ _]eqWi; apply: rsim_irr_comp (socle_irr _). have bij_irr: {on [pred i | soc i], bijective standard_irr}. exists (odflt W0 \o soc) => [Wi _ | i]; first by rewrite /= irrK. by rewrite inE /soc /=; case: pickP => //= Wi; move/eqP. rewrite !(reindex standard_irr) {bij_irr}//=. have all_soc Wi: soc (standard_irr Wi) by rewrite irrK. rewrite (eq_bigr val) => [|Wi _]; last by rewrite /W irrK. rewrite !(eq_bigl _ _ all_soc); split=> //. rewrite (eq_bigr (mxrank \o val)) => [|Wi _]; last by rewrite /W irrK. by rewrite -mxdirectE /= Socle_direct. pose modW i : mxmodule rG (W i) := if soc i is Some Wi as oWi return mxmodule rG (oapp val 0 oWi) then component_mx_module rG (socle_base Wi) else mxmodule0 rG n. apply: mx_rsim_trans (mx_rsim_sym (rsim_submod1 (mxmodule1 rG) _)) _ => //. apply: mx_rsim_dsum (modW) _ defS dxS _ => i. rewrite /W /standard_irr_coef /modW /soc; case: pickP => [Wi|_] /=; last first. rewrite /muln_grepr big_ord0. by exists 0 => [||x _]; rewrite /row_free ?mxrank0 ?mulmx0 ?mul0mx. by move/eqP=> <-; apply: mx_rsim_socle; apply: rsim_irr_comp (socle_irr Wi). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)