proposition: Fact cfextprod_is_linear g : linear (cfextprod g : 'CF(H) -> 'CF(setX G H)).
proof: Proof. Proof using. move=> /= a h1 h2. apply/cfunP=> /= x. by rewrite !cfunE !mulrDr mulrA [g _ * _]mulrC mulrA. 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