proposition: Lemma cfextprod_cfuni p q : '1_[p] \ox '1_[q] = '1_(classX p q).
proof: Proof. Proof using. apply/cfunP => /= x. rewrite cfunE !cfuniCTnE /= cfunElock genGid !inE /= -natrM mulnb. congr ((nat_of_bool _)%:R); rewrite classXE. apply /andP/subsetP => [[ct1 ct2] /= y /imsetP[/= x0 _] ->{y} | /(_ x)]. - rewrite inE; apply/andP. by split; rewrite classes_of_permP permCTP prod_conjg /=; rewrite cycle_type_conjg partnCTE CTpartnK eq_sym ?ct1 ?ct2. - rewrite class_refl => /(_ isT). rewrite inE => /andP[/imsetP[/= y1 _ ->] /imsetP[/= y2 _ ->]]. by rewrite /ct !cycle_type_conjg !permCTP !CTpartnK !eqxx. 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