proposition: Lemma mdeg_tnth_monsY mz i : mdeg (tnth (monsY mz) i) = tnth (monX mz) i.
proof: Proof. rewrite /monsY /monX !tnth_mktuple /mdeg big_tuple. by apply eq_bigr => j _; rewrite -mnm_tnth mnmE. 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