proposition: Lemma map_sympoly_is_scalable : scalable_for (mor \; *:%R) map_sympoly.
proof: Proof. move=> /= r p. apply val_inj; rewrite /= (mpolyE p) raddf_sum /=. apply/mpolyP => m. rewrite mcoeffZ !mcoeff_map_mpoly /= -!rmorphM /=; congr (mor _). rewrite !linear_sum /= mulr_sumr. by apply eq_bigr => i _; rewrite /= !linearZ /=. 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