proposition: Lemma Schur1 (sh : 'P_1) : Schur n0 R sh = \sum_(i < n) 'X_i.
proof: Proof. Proof using. suff -> : sh = colpartn 1 by rewrite -mesym_SchurE mesym1E. by rewrite !intpartn1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau