proposition: Lemma mult_symh_powersum k d m : ('h_k * 'p_d : SF)@_m = (mdeg m == (k + d)%N)%:R * \sum_(i < n) (m i >= d)%:R.
proof: Proof. Proof using. rewrite rmorphM /= /symp_pol !mulr_sumr linear_sum. apply eq_bigr=> i _ /=; rewrite mult_symh_U. by case: eqP => _ //=; rewrite ?mul0r ?mul1r. 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