proposition: Lemma Wedderburn_id_expansion i : 'e_i = #|G|%:R^-1 *: \sum_(x in G) 'chi_i 1%g * 'chi_i x^-1%g *: aG x.
proof: Proof. have Rei: ('e_i \in 'R_i)%MS by apply: Wedderburn_id_mem. have /envelop_mxP[a def_e]: ('e_i \in R_G)%MS; last rewrite -/aG in def_e. by move: Rei; rewrite genmxE mem_sub_gring => /andP[]. apply: canRL (scalerK (neq0CG _)) _; rewrite def_e linear_sum /=. apply: eq_bigr => x Gx; have Gx' := groupVr Gx; rewrite scalerA; congr (_ *: _). transitivity (cfReg G).['e_i *m aG x^-1%g]%CF. rewrite def_e mulmx_suml raddf_sum (bigD1 x) //= -scalemxAl xcfunZr. rewrite -repr_mxM // mulgV xcfunG // cfRegE eqxx mulrC big1 ?addr0 //. move=> y /andP[Gy /negbTE neq_xy]; rewrite -scalemxAl xcfunZr -repr_mxM //. by rewrite xcfunG ?groupM // cfRegE -eq_mulgV1 neq_xy mulr0. rewrite cfReg_sum -xcfun_rE raddf_sum /= (bigD1 i) //= xcfunZl. rewrite xcfun_mul_id ?envelop_mx_id ?xcfunG ?groupV ?big1 ?addr0 // => j ne_ji. rewrite xcfunZl (xcfun_annihilate ne_ji) ?mulr0 //. have /andP[_ /(submx_trans _)-> //] := Wedderburn_ideal (W i). by rewrite mem_mulsmx // envelop_mx_id ?groupV. 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)