proposition: Lemma Newton_syme (k : nat) : k%:R *: 'e_k = \sum_(0 <= i < k) (-1) ^+ (k - i).+1 *: 'e_i * 'p_(k - i) :> SF.
proof: Proof. rewrite Newton_syme1 big_mkord (reindex_inj rev_ord_inj) /=. rewrite big_add1 /= big_mkord; apply eq_bigr => i _. by rewrite mulrC subKn // scalerCA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(ssrcomplements freeg mpoly) sorted tools ordtype permuted partition skewpart composition Yamanouchi std tableau stdtab skewtab permcent antisym Schur_mpoly therule Schur_altdef unitriginv