proposition: Lemma sum_symmE d (f : {sympoly R[n]}) : \sum_(l : 'P_d) f@_(mpart l) *: 'm[l] = \sum_(l <- [seq val p | p <- enum {: 'P_d}]) f@_(mpart l) *: 'm[l].
proof: Proof. by rewrite big_map big_enum. 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