proposition: Lemma sum_syme_symh (d : nat) : d != 0%N -> \sum_(0 <= i < d.+1) (-1) ^+ i *: ('e_i * 'h_(d - i)) = 0 :> SF.
proof: Proof. move=> Hd; rewrite big_nat_rev /=. rewrite -[RHS](scaler0 _ ((-1)^+d)) -[in RHS](sum_symh_syme Hd) scaler_sumr /=. rewrite !big_nat; apply eq_bigr => i /andP[_ Hi]. rewrite mulrC !add0n subSS subKn // scalerA; congr (_ *: ('h__ * 'e__)). by rewrite -signr_odd oddB // signr_addb !signr_odd. 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