proposition: Lemma cfextprod_char g h : g \is a character -> h \is a character -> g \ox h \is a character.
proof: Proof. move=> /char_reprP[rG ->{g}] /char_reprP[rH ->{h}]. apply/char_reprP; exists (Representation (extprod_mx_repr rG rH)). by rewrite /= cfRepr_extprod. 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