proposition: Lemma decomp_cf_triv : \sum_(p : 'P_n) '1_[p] = 1.
proof: Proof. Proof using. apply/cfunP => /= x. rewrite cfun1Egen genGid inE /=. rewrite sum_cfunE (bigD1 (ct x)) //=. rewrite big1 ?addr0 ?cfuniCTnE ?eqxx //=. by move=> p /negbTE pct; rewrite cfuniCTnE eq_sym pct. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg fingroup morphism perm gproduct) mathcomp(ssrnum matrix vector mxalgebra algC) mathcomp(classfun character mxrepresentation) tools ordcast partition sorted permcomp cycles cycletype permcent