proposition: Fact sympolyf_is_linear : linear sympolyf.
proof: Proof. rewrite /sympolyf => /= r u v. case: (SF (r *: u + v)) (SF u) (SF v) => [puv [Hpuv _]] [pu [Hpu _]] [pv [Hpv _]]. apply msym_fundamental_un. by rewrite linearP /= Hpu Hpv Hpuv. 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