proposition: Theorem mcoeff_symbs (la : 'P_d) f : coord symbs (enum_rank la) f = (alternpol 'X_[rho n] * sympol (homsym f))@_(mpart la + rho n).
proof: Proof. have /coord_span -> : f \in span symbs. by rewrite (span_basis symbs_basis) memvf. rewrite !coord_sum_free ?(basis_free symbs_basis) //. rewrite (reindex _ (onW_bij _ (@enum_rank_bij 'P_d))) /=. rewrite !linear_sum /= mulr_sumr linear_sum /= (bigD1 la) //=. rewrite (nth_map (rowpartn d)) -?cardE ?ltn_ord // nth_enum_rank. rewrite -scalerAr linearZ /=. have Hszp (nu : 'P_d) : (size nu <= n)%N. by apply: (leq_trans _ Hd); rewrite -{2}(sumn_intpartn nu) size_part. rewrite mcoeff_alt_SchurE // eq_refl mulr1 big1 ?addr0 // => mu /negbTE Hmula. rewrite (nth_map (rowpartn d)) -?cardE ?ltn_ord // nth_enum_rank. rewrite -scalerAr linearZ /=. by rewrite mcoeff_alt_SchurE // Hmula mulr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg matrix vector ssrnum algC archimedean) mathcomp(fingroup perm) mathcomp(ssrcomplements freeg mpoly) tools sorted ordtype permuted partition permcent antisym Schur_mpoly Schur_altdef sympoly