proposition: Lemma mx_Maschke : [char F]^'.-group G -> mx_completely_reducible 1%:M.
proof: Proof. rewrite /pgroup charf'_nat; set nG := _%:R => nzG U => /mxmoduleP Umod _. pose phi := nG^-1 *: (\sum_(x in G) rG x^-1 *m pinvmx U *m U *m rG x). have phiG x: x \in G -> phi *m rG x = rG x *m phi. move=> Gx; rewrite -scalemxAl -scalemxAr; congr (_ *: _). rewrite {2}(reindex_acts 'R _ Gx) ?astabsR //= mulmx_suml mulmx_sumr. apply: eq_bigr => y Gy; rewrite !mulmxA -repr_mxM ?groupV ?groupM //. by rewrite invMg mulKVg repr_mxM ?mulmxA. have Uphi: U *m phi = U. rewrite -scalemxAr mulmx_sumr (eq_bigr (fun _ => U)) => [|x Gx]. by rewrite sumr_const -scaler_nat !scalerA mulVf ?scale1r. by rewrite 3!mulmxA mulmxKpV ?repr_mxKV ?Umod ?groupV. have tiUker: (U :&: kermx phi = 0)%MS. apply/eqP/rowV0P=> v; rewrite sub_capmx => /andP[/submxP[u ->] /sub_kermxP]. by rewrite -mulmxA Uphi. exists (kermx phi); last exact/mxdirect_addsP. apply/mxmoduleP=> x Gx; apply/sub_kermxP. by rewrite -mulmxA -phiG // mulmxA mulmx_ker mul0mx. apply/eqmxP; rewrite submx1 sub1mx. rewrite /row_full mxrank_disjoint_sum //= mxrank_ker. suffices ->: (U :=: phi)%MS by rewrite subnKC ?rank_leq_row. apply/eqmxP; rewrite -{1}Uphi submxMl scalemx_sub //. by rewrite summx_sub // => x Gx; rewrite -mulmxA mulmx_sub ?Umod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)