proposition: Theorem cfuni_Res (l : 'P_(m + n)) : 'Res[tinj @* ('dom tinj)] '1_[l] = \sum_(pp | l == pp.1 +|+ pp.2) '1_[pp.1] \o^ '1_[pp.2].
proof: Proof. Proof using. apply/cfunP => /= s. case: (boolP (s \in tinj @* ('dom tinj))) => Hs; first last. by rewrite !cfun0gen // genGid. rewrite (cfResE _ _ Hs); last exact: subsetT. move: Hs => /imsetP/= [[s1 s2]]. rewrite inE => /andP[H1 _] -> {s}. rewrite cfuni_tinj /= -linear_sum (cfIsomE _ _ H1). rewrite /cfextprod /= sum_cfunE. symmetry; transitivity (\sum_(pp | l == pp.1 +|+ pp.2) '1_[pp.1] s1 * '1_[pp.2] s2). by apply eq_bigr => i _; rewrite cfunE. case: (altP eqP) => [->| Hl] /=. - rewrite (bigD1 (ct s1, ct s2)) //=. rewrite !cfuniCTnE !eqxx /= mulr1. rewrite big1 ?addr0 // => [[t1 t2]] /andP[_]. rewrite !cfuniCTnE eq_sym xpair_eqE. by move=> /nandP[] /negbTE -> /=; rewrite ?mulr0 ?mul0r. - rewrite big1 // => [[t1 t2]] /= /eqP Hll; subst l. have {Hl} : (t1, t2) != (ct s1, ct s2). by move: Hl; apply contra => /eqP[-> ->]. rewrite !cfuniCTnE eq_sym xpair_eqE. by move=> /nandP[] /negbTE -> /=; rewrite ?mulr0 ?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