proposition: Fact sympolyf_is_multiplicative : multiplicative sympolyf.
proof: Proof. rewrite /sympolyf; split. - move=> u v. case: (SF (u * v)) (SF u) (SF v) => [puv [Hpuv _]] [pu [Hpu _]] [pv [Hpv _]]. apply msym_fundamental_un. by rewrite [RHS]rmorphM /= -/(pu \mPo _) -/(pv \mPo _) Hpu Hpv Hpuv. - case: (SF 1) => [p1 [Hp1 _]]. by apply msym_fundamental_un; rewrite Hp1 comp_mpoly1. 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