proposition: Lemma Schur_cast d d' (la : 'P_d) (Heq : d = d') : Schur n0 R (cast_intpartn Heq la) = 's_[la].
proof: Proof. Proof using . by subst d'; congr Schur. 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