proposition: Theorem Schur_sym d (la : 'P_d) : 's_la \is symmetric.
proof: Proof. Proof using . have -> : 's_la = map_mpoly intr (Schur _ int la). rewrite /Schur /polylang /commword raddf_sum /=; apply eq_bigr => i _ /=. by rewrite rmorph_prod /=; apply eq_bigr => {}i _ ; rewrite map_mpolyX. apply/issymP => s. have:= Schur_sym_idomain n0 int la => /issymP/(_ s) {2}<-. by rewrite msym_map_mpoly. 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