proposition: Lemma Fchar_invK : cancel Fchar_inv Fchar.
proof: Proof. Proof using Hn. move=> p; rewrite !Fchar_invE linear_sum. have: p \in span 'hp. by rewrite (span_basis (symbp_basis Hn _ )) // memvf. move=> /coord_span {2}->. rewrite (reindex _ (onW_bij _ (@enum_rank_bij 'P__))) /=. apply eq_bigr => i _. rewrite linearZ /= Fchar_ncfuniCT; congr (_ *: _). rewrite (nth_map inh); last by rewrite -cardE ltn_ord. by congr ('hp[_]); rewrite -enum_val_nth enum_rankK. 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