proposition: Lemma symm_homog d (sh : 'P_d) : sympol 'm[sh] \is d.-homog.
proof: Proof. Proof using. case: (leqP (size sh) n) => [Hsz | /symm_oversize ->]; last exact: dhomog0. rewrite /= unfold_in; apply/allP => /= m. rewrite mcoeff_msupp mcoeff_symm //. case: (boolP (perm_eq _ _)) => [Hperm _ | _]; last by rewrite /= eq_refl. rewrite /mdeg -sumnE -(sumn_intpartn sh). move: Hperm => /perm_sumn <-{m}. rewrite -{2}(mpartK _ Hsz) // is_dominant_partm; last exact: mpart_is_dominant. apply/eqP; rewrite /= !sumnE big_filter. rewrite [LHS](bigID (fun i => i == 0%N)) /= big1 ?add1n //. by move=> i /eqP. 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