proposition: Lemma msym_pihomog d p (s : 'S_n) : msym s (pihomog mdeg d p) = pihomog mdeg 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 < n] = mdeg m. by apply/perm_big/tuple_permP; exists (s^-1)%g. by case: (mdeg m == d); rewrite ?msym0 ?msymX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg