proposition: Lemma homsyme_character (la : 'P_n) : Fchar_inv 'he[la] \is a character.
proof: Proof. rewrite -omega_homsymh; first last. by apply: (leq_trans _ Hn); rewrite -{2}(sumn_intpartn la) leq_head_sumn. rewrite omega_Fchar_inv //. exact: (rpredM (lin_charW sign_charP) (homsymh_character _)). 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