proposition: Lemma FcharK : cancel Fchar Fchar_inv.
proof: Proof. Proof using Hn. move=> f. rewrite !Fchar_invE {2}(ncfuniCT_gen f); apply eq_bigr => la _. rewrite FcharE; congr (_ *: _). rewrite (reindex _ (onW_bij _ (@enum_val_bij _))) /=. transitivity (coord 'hp (enum_rank la) (\sum_(j < #|{:'P_n}|) (f (permCT (enum_val j)) / 'z_(enum_val j)) *: ('hp`_j : HS))). congr coord; apply eq_bigr => /= i _; congr (_ *: _). rewrite (nth_map inh); last by rewrite -cardE ltn_ord. by congr ('hp[_]); apply enum_val_nth. by rewrite coord_sum_free ?enum_rankK //; exact: symbp_free. 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