proposition: Theorem Frobenius_char_homsymdot la (sigma : 'S_n) : 'irrSG[la] sigma = '[ 'hs[la] | 'hp[cycle_typeSn sigma] ] _(n.-1, n).
proof: Proof. rewrite cfdotr_ncfuniCT -(Fchar_isometry (leqSpred n)). by rewrite Fchar_irrSGE Fchar_ncfuniCT. 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