proposition: Lemma cfextprodDl h g1 g2 : (g1 + g2) \ox h = g1 \ox h + g2 \ox h.
proof: Proof. Proof using. by rewrite -!cfextprodrE linearD. 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