proposition: Theorem MN_coeffP d (la : 'P_d) : 'p[la] = \sum_(sh : 'P_d) (MN_coeff sh la)%:~R *: 's[sh] :> SF.
proof: Proof. rewrite -(map_symp_prod intr) MN_coeffP_int rmorph_sum /=. by under [LHS]eq_bigr do rewrite linearZ /= 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