proposition: Theorem alt_uniq d (la : 'P_d) (s : {mpoly R[n]}) : size la <= n -> 'a_rho * s = 'a_(mpart la + rho) -> s = 's_la.
proof: Proof. Proof using . by move=> /(alt_SchurE R) <- /(mulfI (alt_rho_non0 n R)). 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