proposition: Fact cfextprod_subproof (g : 'CF(G)) (h : 'CF(H)) : is_class_fun <<setX G H>> [ffun x => g x.1 * h x.2].
proof: Proof. Proof using. rewrite genGid; apply intro_class_fun => [x y|]. - rewrite !inE => /andP[x1 x2] /andP[y1 y2]. by rewrite !cfunJgen ?genGid. - move=> x; rewrite inE => /nandP[x1|x2]. + by rewrite cfun0gen ?mul0r ?genGid. + by rewrite [h _]cfun0gen ?mulr0 ?genGid. 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