proposition: Fact map_sympoly_d_homog (p : HSFR) : map_sympoly mor p \is d.-homsym.
proof: Proof. rewrite homsymE /=; apply/dhomogP => /= m. rewrite mcoeff_msupp mcoeff_map_mpoly => Hm. have {Hm} : p@_m != 0. move: Hm; apply contra => /eqP ->. by apply/eqP; apply: (rmorph0 mor). rewrite -mcoeff_msupp => Hm. by have /dhomogP/(_ _ Hm) := homsym_is_dhomog p. 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