proposition: Theorem Frobenius_char_coord la (sigma : 'S_n) : 'irrSG[la] sigma = coord 'hs (enum_rank la) ('hp[cycle_typeSn sigma] : {homsym algC[n.-1.+1, n]}).
proof: Proof. pose HSC := {homsym algC[n.-1.+1, n]}. symmetry. rewrite Frobenius_char_homsymdot. have /coord_span {2}-> : ('hp[cycle_typeSn sigma] : HSC) \in span 'hs. by rewrite (span_basis (symbs_basis _ (leqSpred n))) // memvf. rewrite (reindex _ (onW_bij _ (@enum_rank_bij 'P__))) /=. rewrite homsymdot_sumr (bigD1 la) //=. rewrite (nth_map (rowpartn n)) -?cardE ?ltn_ord // nth_enum_rank. rewrite homsymdotZr homsymdotss ?leqSpred // eq_refl mulr1. rewrite big1 ?addr0; first last. move=> nu /negbTE Hnu. rewrite (nth_map (rowpartn n)) -?cardE ?ltn_ord // nth_enum_rank. by rewrite homsymdotZr homsymdotss ?leqSpred // eq_sym Hnu mulr0. by rewrite -coord_map_homsym ?map_homsymbs ?symbs_basis // map_homsymp. 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