proposition: Lemma Fchar_ncfuniCT (l : 'P_n) : Fchar '1z_[l] = 'hp[l].
proof: Proof. Proof using. rewrite !FcharE (bigD1 l) //= big1 ?addr0; first last. move=> m /negbTE Hm /=. rewrite cfunElock cfuniCTE /= permCTP partnCTE /= !CTpartnK Hm /=. by rewrite mulr0 mul0r scale0r. rewrite cfunElock cfuniCTE /= permCTP eq_refl /=. by rewrite mulr1 divff ?scale1r. 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