proposition: Lemma rem_irr (xi phi : 'CF('SG_n)) : xi \in irr 'SG_n -> phi \is a character -> phi - '[phi, xi] *: xi \is a character.
proof: Proof. move=> Hxi Hphi. have /natrP[m Hm] := Cnat_cfdot_char Hphi (irrWchar Hxi). rewrite Hm. elim: m phi Hphi Hm => [|m IHm] phi Hphi Hm; first by rewrite scale0r subr0. rewrite mulrS scalerDl scale1r opprD addrA; apply: IHm. - by apply rem_irr1; rewrite //= Hm pnatr_eq0. - by rewrite cfdotBl Hm irrWnorm // mulrS [1 + _]addrC addrK. 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