proposition: Lemma symHE_intpartn d : E d = \sum_(la : 'P_d) (-1)^+(d - size la) * (perm_partn la)%:R *: prod_gen H la.
proof: Proof. rewrite symHE_intcompn; symmetry. transitivity (\sum_(la : 'P_d) (\sum_(c : intcompn d | sort geq c == la) (-1) ^+ (d - size c) *: prod_gen H la)). apply eq_bigr => la _; rewrite /perm_partn -sum1_card. rewrite natr_sum mulr_sumr -scaler_suml; congr (_ *: _). apply eq_big => /= co; rewrite inE //= => /eqP <-. rewrite mulr1; congr (_ ^+ (d - _)). by apply: perm_size; rewrite perm_sort. rewrite (exchange_big_dep xpredT) //=. apply eq_bigr => la _. rewrite (eq_bigl (xpred1 (partn_of_compn la))) ?big_pred1_eq //. by move=> mu; rewrite eq_sym -val_eqE. 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