proposition: Theorem Frobenius_char n (la mu : 'P_n) : 'irrSG[la] (permCT mu) = (Vanprod * \prod_(d <- mu) (symp_pol n algC d))@_(mpart la + rho n).
proof: Proof. rewrite -/Vanprod Vanprod_alt. case: n la mu => [//|n] //= la mu. rewrite (charSG0 (irrSG_irr _)) cfun1E inE /=. rewrite !mnm_n0E !intpartn0 {la mu} rowpartn0E big_nil mulr1. by rewrite mcoeff_alt //= map_inj_in_uniq ?enum_uniq // => /= [[]]. rewrite Frobenius_char_coord cycle_typeSn_permCT. by rewrite mcoeff_symbs ?leqSpred //= rmorph_prod. 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