proposition: Lemma Fchar_triv : Fchar 1 = 'hh[rowpartn n].
proof: Proof. rewrite -decomp_cf_triv linear_sum. rewrite (eq_bigr (fun la => 'z_la^-1 *: 'hp[la])); first last => [la _|]. rewrite -Fchar_ncfuniCT /ncfuniCT /= linearZ /=. by rewrite scalerA /= mulrC divff // scale1r. apply val_inj; case: n => [|n0]/=. rewrite prod_gen0 (big_pred1 (rowpartn 0)); first last. by move=> la /=; rewrite !intpartn0 eqxx. rewrite linearZ /= prod_gen0. rewrite zcoeffE /zcard rowpartn0E big_nil mul1n /=. by rewrite big1 // invr1 scale1r. rewrite /prod_gen rowpartnE big_seq1 raddf_sum symh_to_symp //=. by apply eq_bigr => l _; rewrite zcoeffE. 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