proposition: Lemma homog_symmE d (f : {sympoly R[n]}) : sympol f \is d.-homog -> f = \sum_(l : 'P_d) f@_(mpart l) *: 'm[l].
proof: Proof. move=> Hhomog; rewrite {1}(sym_symmE f). apply val_inj => /=. rewrite !linear_sum /= (bigID (fun i : 'P_d => mpart i \in msupp f)) /=. rewrite [X in _ + X]big1 ?addr0; last by move=> i /memN_msupp_eq0 ->; rewrite scale0r. under [RHS]eq_bigr => i Hi. rewrite -{2}(@mpartK n i) //; last exact: (size_mpart_in_supp Hhomog). over. rewrite /=. transitivity (\sum_(m <- [seq mpart i | i : 'P_d ] | m \in msupp f) f@_m *: sympol ('m[partm m])); first last. by rewrite big_map big_enum_cond. rewrite -big_filter -[RHS]big_filter; apply perm_big; apply uniq_perm. - by apply filter_uniq; apply msupp_uniq. - rewrite filter_map map_inj_in_uniq; first by apply filter_uniq; apply enum_uniq. move=> /= c1 c2; rewrite !mem_filter /= => /andP[Hc1 _] /andP[Hc2 _]. move=> /(congr1 (@partm n)) /(congr1 val) /=. rewrite !mpartK // ?(size_mpart_in_supp _ Hc1) ?(size_mpart_in_supp _ Hc2) //. exact: val_inj. - move=> /= m; rewrite !mem_filter andbC. case: (boolP (m \in msupp f)) => //= Hsupp. apply/idP/mapP => /= [Hdom | [l _ ->]]; last exact: mpart_is_dominant. have {Hsupp} degm : mdeg m = d. by move: Hhomog => /dhomogP/(_ _ Hsupp). have {Hdom degm} [p ->] := dominant_mpart Hdom degm. by exists p => //; rewrite mem_enum. 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