proposition: Lemma Schur_freeSchurE d (Q : stdtabn d) : Schur (shape_deg Q) = polylang R (freeSchur Q).
proof: Proof. Proof using . rewrite SchurE -tabword_of_tuple_freeSchur. rewrite /polylang (big_imset _ (@tabword_of_tuple_freeSchur_inj _ Q)) /=. apply: eq_bigr => t _; apply: perm_commword. by rewrite perm_sym; exact: perm_RS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly