proposition: Lemma evalE (R : ringType) m w : (\prod_(v <- w) 'X_v)@_m = (eval w == m)%:R :> R.
proof: Proof. rewrite -[X in X@_m](big_map (fun i : 'I_n.+1 => (U_(i))%MM) xpredT). rewrite /eval mpolyX_prod mcoeffX; congr (nat_of_bool _)%:R. apply/eqP/eqP => [/(congr1 val) /= <-{m} | H]. - elim: w => [| w0 w IHw] /=; first by rewrite big_nil. rewrite big_cons; apply eq_from_tnth => i. move/(congr1 (fun t => tnth t i)) : IHw; rewrite !tnth_mktuple => ->. by rewrite mnmE -mnm_tnth. - apply val_inj => /=; rewrite -{m}H. elim: w => [| w0 w IHw] /=; first by rewrite big_nil. rewrite big_cons; apply eq_from_tnth => i. move/(congr1 (fun t => tnth t i)) : IHw. by rewrite !tnth_mktuple mnmE -mnm_tnth => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn