proposition: Lemma cfDetRepr n rG : cfDet (cfRepr rG) = @detRepr _ _ n rG.
proof: Proof. transitivity (\prod_W detRepr (socle_repr W) ^+ standard_irr_coef rG W). rewrite (reindex _ (socle_of_Iirr_bij _)) unlock /=. apply: eq_bigr => i _; congr (_ ^+ _). rewrite (cfRepr_sim (mx_rsim_standard rG)) cfRepr_standard. rewrite cfdot_suml (bigD1 i) ?big1 //= => [|j i'j]; last first. by rewrite cfdotZl cfdot_irr (negPf i'j) mulr0. by rewrite cfdotZl cfnorm_irr mulr1 addr0 natrK. apply/cfun_inP=> x Gx; rewrite prod_cfunE //. transitivity (detRepr (standard_grepr rG) x); last first. rewrite !cfunE Gx !trace_mx11 !mxE eqxx !mulrb. case: (standard_grepr rG) (mx_rsim_standard rG) => /= n1 rG1 [B Dn1]. rewrite -{n1}Dn1 in rG1 B *; rewrite row_free_unit => uB rG_B. by rewrite -[rG x](mulmxK uB) rG_B // !det_mulmx mulrC -!det_mulmx mulKmx. rewrite /standard_grepr; elim/big_rec2: _ => [|W y _ _ ->]. by rewrite cfunE trace_mx11 mxE Gx det1. rewrite !cfunE Gx /= !{1}trace_mx11 !{1}mxE det_ublock; congr (_ * _). rewrite exp_cfunE //; elim: (standard_irr_coef rG W) => /= [|k IHk]. by rewrite /muln_grepr big_ord0 det1. rewrite exprS /muln_grepr big_ord_recl det_ublock -IHk; congr (_ * _). by rewrite cfunE trace_mx11 mxE Gx. 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)