proposition: Lemma omegasf_syms la : d <= n -> omegasf 's[la] = 's[conj_intpartn la].
proof: Proof. move=> ledn. rewrite syms_symh raddf_sum /= syms_syme. apply eq_bigr => /= s _. rewrite linearZ /= omegasf_prodsymh //. apply: (leq_trans _ ledn). rewrite -{2}(sumn_intpartn s). by case: s => [[|s0 s]//= _]; rewrite leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv