proposition: Fact extprod_mx_repr_subproof : mx_repr (setX G H) (fun x => tprod (rG x.1) (rH x.2)).
proof: Proof. Proof using. split=>[|i j]; first by rewrite !repr_mx1 tprod1. rewrite !inE => /andP[i1 i2] /andP[j1 j2]. by rewrite !repr_mxM // tprodE. 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