proposition: Theorem dim_irrSG n (la : 'P_n) : 'irrSG[la] 1%g = #|{: stdtabsh la}|%:R.
proof: Proof. pose HSC := {homsym algC[n.-1.+1, n]}. rewrite -permCT_colpartn Frobenius_char_coord cycle_typeSn_permCT. have -> : 'hp[colpartn n] = 'hh[colpartn n] :> HSC. apply val_inj; rewrite /= !prod_gen_colpartn. by rewrite sympe1E -symhe1E. have -> : 'hh[colpartn n] = \sum_la 'K(la, colpartn n) *: 'hs[la] :> HSC. apply val_inj. by rewrite /= linear_sum /= -![prod_gen _ _]/('h[_]) symh_syms. rewrite (reindex _ (onW_bij _ (@enum_val_bij _))) /=. rewrite (eq_bigr (fun i : 'I__ => 'K(enum_val i, colpartn n) *: 'hs`_i)); first last. move=> /= i _. rewrite (nth_map inh); last by rewrite -cardE ltn_ord. by congr (_ *: 'hs[_]); apply enum_val_nth. by rewrite coord_sum_free ?enum_rankK // ?KostkaStd //; exact: symbs_free. 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