proposition: Theorem Schur_sym_idomain d (la : 'P_d) : 's_la \is symmetric.
proof: Proof. Proof using . case: (leqP (size la) n) => [Hla|]. - have := alt_anti R (mpart la + rho). rewrite -(alt_SchurE _ Hla) -sym_antiE //; last exact: alt_anti. exact: alt_rho_non0. - move/Schur_oversize ->; exact: rpred0. 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