proposition: Lemma syms_sympM_oapp d (la : 'P_d) m : m != 0%N -> 's[la] * 'p_m = \sum_(i < n) oapp (fun ph => (-1) ^+ ph.2.-1 *: 's[ph.1]) 0 (add_ribbon_intpartn la m.-1 i) :> SF.
proof: Proof. move=> Hm. case: (leqP (size la) n) => szla; first last. rewrite syms_oversize // mul0r; apply/esym/big1 => /= i _. case Haddrib: add_ribbon_intpartn => [[sh h]|]//=. move/add_ribbon_intpartnP in Haddrib. rewrite syms_oversize ?scaler0 //. by rewrite (size_add_ribbon Haddrib) leq_max szla. rewrite -(map_syms intr) -(map_symp intr). rewrite -rmorphM syms_sympM_oapp_int // rmorph_sum /=. apply eq_bigr => i _. case: add_ribbon_intpartn => [p|]/=; last by rewrite rmorph0. by rewrite linearZ /= rmorphXn rmorphN1 map_syms. 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