proposition: Lemma omega_Fchar_inv (p : HS) : Fchar_inv (omegahomsym p) = sign_char * (Fchar_inv p).
proof: Proof. have /coord_span -> : p \in span 'hp. by rewrite (span_basis (symbp_basis Hn _ )) // memvf. rewrite !linear_sum /= mulr_sumr; apply eq_bigr => i _. rewrite !linearZ /= -scalerAr; congr (_ *: _). rewrite {p} (nth_map (rowpartn n)); last by rewrite -cardE ltn_ord. move: (nth _ _ _) => la {i}. rewrite omega_homsymp //; try by apply: (leq_trans (leq_head_sumn _)); rewrite sumn_intpartn. rewrite linearZ /= Fchar_inv_homsymp. rewrite /ncfuniCT scalerA mulrC -scalerA -scalerAr; congr (_ *: _). rewrite -cfunP => /= s; rewrite !cfunE. rewrite odd_cycle_type signr_odd sumn_intpartn. rewrite cfuniCTE; case: eqP => [->|]; rewrite /= ?mulr0 // {s}. by rewrite {1}card_ord cast_intpartnE. 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