proposition: Lemma homsymh_character (la : 'P_n) : Fchar_inv 'hh[la] \is a character.
proof: Proof. move: (n) la Hn => d [la /= Hla]. have:= Hla => /andP[/eqP Hd _]; subst d. elim: la Hla => [| l0 la IHla] Hlla Hd. by rewrite intpartn0 -Fchar_triv FcharK // cfun1_char. have Hla : (sumn la == sumn la) && is_part la. by rewrite eq_refl /=; have:= Hlla => /andP[_ /is_part_consK ->]. have Hdla : (sumn la <= nvar)%N by apply: (leq_trans _ Hd); rewrite /= leq_addl. have {IHla} Hrec := IHla Hla Hdla. rewrite homsymprod_hh -Fchar_triv -(Fchar_invK Hdla 'hh[(IntPartN Hla)]). rewrite -Fchar_ind_morph (FcharK Hd). apply cfInd_char; rewrite cfIsom_char. exact: (cfextprod_char (cfun1_char _) Hrec). 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