proposition: Theorem dim_cfReprSG n (la : 'P_n) d (rG : mx_representation algC 'SG_n d) : cfRepr rG = 'irrSG[la] -> d = #|{: stdtabsh la}|.
proof: Proof. move=> H; have := cfRepr1 rG; rewrite H dim_irrSG => /eqP. by rewrite eqC_nat => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama