proposition: Lemma cfRepr_extprod : cfRepr extprod_mx_repr = cfRepr rG \ox cfRepr rH.
proof: Proof. Proof using. apply/cfun_inP=> x GXHx. by have:= GXHx; rewrite !inE !cfunE GXHx mxtrace_prod => /andP[-> ->] /=. 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