proposition: Lemma cfdotr_ncfuniCT k (f : 'CF('SG_k)) (s : 'S_k) : (f s) = '[f, '1z_[ct s]].
proof: Proof. Proof using. rewrite {2}(ncfuniCT_gen f) cfdot_suml. rewrite (bigD1 (ct s)) //= !cfdotZl cfdotZr. rewrite mulrA (divfK _) //. rewrite cfdot_cfuni; try (by apply: class_normal; rewrite inE). rewrite setIid big1 ?addr0. - have: (permCT (ct s)) \in s ^: 'SG_k. rewrite classes_of_permP permCTP. by rewrite (partnCTK (cycle_type s)). move/imsetP => [y _ ->]; rewrite cfunJgen ?genGid ?inE //. rewrite fmorph_div !conjC_nat !mulrA divfK ?pnatr_eq0 ?card_classCT_neq0 //. by rewrite mulfK // neq0CG. - move=> p /negbTE pct. rewrite !cfdotZl cfdotZr. rewrite cfdot_cfuni; try (by apply: class_normal; rewrite inE). rewrite class_disj; first by rewrite cards0 mul0r !mulr0. apply/negP; rewrite classes_of_permP !permCTP. by rewrite partnCTE !CTpartnK 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