proposition: Lemma evalXY_XE mz : 'X_[mz](XY) = 'X_[monX mz](X) * \prod_(i < m) 'X_[tnth (monsY mz) i](Y).
proof: Proof. rewrite -rmorph_prod polyXY_scale /monX. transitivity (\prod_(i : 'I_(m*n)) (('X_(vecmx_index i).2 : polY) ^+ mz i *: ('X_(vecmx_index i).1(X) ^+ mz i))). rewrite (multinomUE_id mz) /evalXY mmapX /mmap1. by apply eq_bigr => [i _]; rewrite -exprZn polyXY_scale. rewrite big_mxvec_index /=. rewrite mpolyXE_id rmorph_prod -scaler_prod; apply eq_bigr => i _. rewrite scaler_prod /=; congr (_ *: _). - rewrite /monsY tnth_mktuple mpolyXE_id; apply eq_bigr => j _. by rewrite mxvec_indexK /= mnmE. - rewrite mnmE -prodrXr rmorph_prod /=; apply eq_bigr => j _. by rewrite mxvec_indexK /= rmorphXn. 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