proposition: Theorem irrSG_irr la : 'irrSG[la] \in irr 'SG_n.
proof: Proof. elim/(finord_wf_down (T := 'PDom_n)): la => la IHla. rewrite irrEchar irrSG_orthonormal !eq_refl andbT. have -> : 'irrSG[la] = 'M[la] - \sum_(mu : 'PDom_n | (la < mu)%O) '[ 'M[la], 'irrSG[mu] ] *: 'irrSG[mu]. apply/eqP; rewrite eq_sym subr_eq {1}Young_rule_partdom. apply/eqP; congr (_ + _); apply eq_bigr => mu _. rewrite Young_rule. rewrite cfdot_suml (bigD1 mu) //= cfdotZl. rewrite irrSG_orthonormal eq_refl mulr1 scalerDl. rewrite big1 ?scale0r ?addr0 // => nu /negbTE Hnu. by rewrite cfdotZl irrSG_orthonormal Hnu mulr0. rewrite -big_filter; set L := filter _ _. have : all (<%O la) L by apply filter_all. have : uniq L by apply: filter_uniq; apply: index_enum_uniq. elim: L => [| l0 l IHl]. by rewrite big_nil subr0 homsymh_character. rewrite big_cons /= => /andP[Hl0l Huniq] /andP[Hl0 Hall]. rewrite [X in 'M[la] - X]addrC opprD addrA. have {IHl Huniq Hall} := IHl Huniq Hall. set Frec := 'M[la] - _ => HFrec. suff {IHla} -> : '['M[la], 'irrSG[l0]] = '[Frec, 'irrSG[l0]]. by apply rem_irr => //; apply: IHla. rewrite {HFrec}/Frec /= cfdotBl /=. rewrite cfdot_suml big_seq big1 ?cfdot0l ?subr0 // => mu Hmu. rewrite cfdotZl irrSG_orthonormal. case: eqP => H; last by rewrite mulr0. by rewrite -H Hmu in Hl0l. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism gproduct) mathcomp(rat ssralg ssrint ssrnum algC vector archimedean) mathcomp(mxrepresentation classfun character) mathcomp(mpoly) sorted ordtype tools partition antisym sympoly homogsym Cauchy Schur_altdef stdtab therule permcomp cycletype towerSn permcent reprSn unitriginv MurnaghanNakayama