proposition: Lemma zcoeffE k (l : 'P_k) : zcoeff l = (zcard l)%:R.
proof: Proof. rewrite /zcoeff card_class_of_part cardsT card_Sn. rewrite char0_natf_div; [| exact: Cchar | exact: dvdn_zcard_fact]. rewrite invf_div mulrC mulfVK //. by rewrite pnatr_eq0 -lt0n; apply: fact_gt0. 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