proposition: Theorem Murnaghan_Nakayama_char n la (sigma : 'S_n) : 'irrSG[la] sigma = (MN_coeff la (cycle_typeSn sigma))%:~R.
proof: Proof. rewrite Frobenius_char_homsymdot MN_coeff_homogP raddf_sum /=. rewrite (bigD1 la) //= big1 ?addr0 //; first last => [i /negbTE Hi|]. by rewrite homsymdotZr homsymdotss // eq_sym Hi mulr0. rewrite homsymdotZr homsymdotss // eqxx mulr1. by rewrite Num.Theory.conj_intr // intr_int. 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