proposition: Lemma cfdot_Ind_cfuniCT p q (l : 'P_(m + n)) : '[ 'Ind['SG_(m + n)] ('1_[p] \o^ '1_[q]), '1_[l] ] = (p +|+ q == l)%:R / 'z_p / 'z_q.
proof: Proof. Proof using. rewrite -cfdot_Res_r cfuni_Res -linear_sum cfIsom_iso cfdot_sumr. transitivity (\sum_(i | l == i.1 +|+ i.2) #|(classX p q) :&: (classX i.1 i.2)|%:R / #|SnXm|%:R : algC). apply eq_bigr => i _; rewrite !cfextprod_cfuni. by rewrite cfdot_cfuni //=; apply: class_normal; rewrite !inE. case: (boolP (p +|+ q == l)) => [|] /= unionp; [rewrite mul1r|rewrite !mul0r]. - rewrite (bigD1 (p, q)) /=; last by rewrite eq_sym. rewrite setIid big1. rewrite addr0 classXE !cardsX natrM /zcoeff. rewrite !invfM !invrK. rewrite [_ * #|classCT p|%:R]mulrC -!mulrA; congr (_ * _). by rewrite [RHS]mulrA [RHS]mulrC natrM invfM. by move=> i /andP[_ ip]; rewrite classXI ?cards0 ?mul0r. - rewrite big1 //= => i /eqP unioni. have ip: i != (p, q). move: unionp; apply contraR; rewrite negbK {}unioni => /eqP. by case: i => [i1 i2] [-> ->]. by rewrite classXI ?cards0 ?mul0r. 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