proposition: Lemma Fchar_irrSGE nvar0 la : Fchar nvar0 'irrSG[la] = 'hs[la].
proof: Proof. rewrite /irrSG -(FcharNvar (nvar0 := n.-1) _) ?leqSpred //=. by rewrite Fchar_invK ?leqSpred //= cnvarhomsyms ?leqSpred. 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