proposition: Lemma cfextprod_suml h I r (P : pred I) (phi : I -> 'CF(G)) : (\sum_(i <- r | P i) phi i) \ox h = \sum_(i <- r | P i) phi i \ox h.
proof: Proof. Proof using. by rewrite -!cfextprodrE linear_sum. 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