proposition: Lemma ncfuniCT_gen k (f : 'CF('SG_k)) : f = \sum_(p : 'P_k) f (permCT p) / 'z_p *: '1z_[p].
proof: Proof. Proof using. apply/cfunP => /= x. rewrite (bigD1 (ct x)) //= cfunE sum_cfunE big1. - rewrite addr0 !cfunE cfuniCTnE eqxx /= mulr1. rewrite -mulrA [_^-1 *_]mulrC mulrA mulfK //. have: (permCT (ct x)) \in x ^: 'SG_k. rewrite classes_of_permP permCTP. by rewrite (partnCTK (cycle_type x)). by move/imsetP => [y _ ->]; rewrite cfunJgen ?genGid ?inE. - by move=> p /negbTE pct; rewrite !cfunE cfuniCTnE eq_sym pct /= !mulr0. 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