proposition: Theorem syms_prod_sympM dn (nu : 'P_dn) dm (mu : 'P_dm) : 's[nu] * 'p[mu] = \sum_(la : 'P_(dn + dm)) (MN_coeff_rec la nu mu)%:~R *: 's[la] :> SF.
proof: Proof. rewrite -(map_syms intr) -(map_symp_prod intr). rewrite -rmorphM syms_prod_sympM_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