proposition: Lemma sympXY k : 'p_k(XY) = 'p_k(X) * 'p_k(Y).
proof: Proof. rewrite /= /symp_pol /= /evalXY /= !rmorph_sum /= big_mxvec_index /=. rewrite [RHS]mulr_suml; apply eq_bigr => i _ /=. rewrite [RHS]mulr_sumr; apply eq_bigr => j _ /=. by rewrite !rmorphXn /= mmapX mmap1U mxvec_indexK /= exprMn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent