proposition: Lemma sym_fundamental_homog (p : {mpoly R[n]}) (d : nat) : p \is symmetric -> p \is d.-homog -> { t | t \mPo S = p /\ t \is d.-homog for mnmwgt }.
proof: Proof. move/sym_fundamental => [t [tSp _]] homp. exists (pihomog mnmwgt d t); split. + by rewrite -pihomog_mPo tSp pihomog_dE. + exact: pihomogP. 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