proposition: Corollary homsyms_homsympM dn (nu : 'P_dn) dm (mu : 'P_dm) : 'hs[nu] *h 'hp[mu] = \sum_(la : 'P_(dn + dm)) (MN_coeff_rec la nu mu)%:~R *: 'hs[la] :> HSF.
proof: Proof. apply val_inj => /=; apply val_inj => /=. have /= := congr1 val (syms_prod_sympM nu mu); rewrite /prod_symp => ->. by rewrite !raddf_sum. 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