proposition: Lemma msym_pihomog nv s (p : {mpoly R[nv]}) : msym s ('pi_d p) = 'pi_d (msym s p).
proof: Proof. rewrite (mpolyE p) ![_ (\sum_(m <- msupp p) _)]linear_sum /=. rewrite [msym s _]linear_sum linear_sum /=. apply eq_bigr => m _; rewrite !linearZ /=; congr (_ *: _). rewrite msymX !pihomogX /=. have -> : mdeg [multinom m ((s^-1)%g i) | i < nv] = mdeg m. rewrite /mdeg; apply perm_big. by apply/tuple_permP; exists (s^-1)%g. by case: (mdeg m == d); rewrite ?msym0 ?msymX. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg matrix vector ssrnum algC archimedean) mathcomp(fingroup perm) mathcomp(ssrcomplements freeg mpoly) tools sorted ordtype permuted partition permcent antisym Schur_mpoly Schur_altdef sympoly