proposition: Lemma syms_sympM_pmap d (la : 'P_d) m : m != 0%N -> 's[la] * 'p_m = \sum_(ph <- pmap (add_ribbon_intpartn la m.-1) (iota 0 n)) (-1) ^+ ph.2.-1 *: 's[ph.1] :> SF.
proof: Proof. move=> Hm; rewrite syms_sympM_oapp //. by rewrite big_pmap -[n in iota 0 n](subn0 n) -/(index_iota 0 n) big_mkord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint perm fingroup tuple vector rat) mathcomp(ssrcomplements freeg mpoly monalg) sorted tools ordtype permuted partition skewpart antisym Schur_mpoly Schur_altdef sympoly homogsym