proposition: Lemma syms_sympM_oapp_int d (la : 'P_d) m : m != 0%N -> size la <= 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. case: m => // m _ szla; apply val_inj. rewrite /= !raddf_sum /=. apply: (mulfI (alt_rho_non0 n _)). rewrite mulrA alt_SchurE //= [LHS]mult_altern_oapp //. rewrite mulr_sumr; apply eq_bigr => mu _. rewrite add_ribbon_intpartnE. case Haddrib: add_ribbon_intpartn => [[sh h]|]/=; last by rewrite mulr0. move/add_ribbon_intpartnP in Haddrib. rewrite -scalerAr alt_SchurE //. by rewrite (size_add_ribbon Haddrib) geq_max szla ltn_ord. 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