proposition: Lemma prod_homog nv l (df : 'I_l -> nat) (mf : 'I_l -> {mpoly R[nv]}) : (forall i : 'I_l, mf i \is (df i).-homog) -> \prod_(i < l) mf i \is (\sum_(i < l) df i).-homog.
proof: Proof. Proof using . elim: l => [| l IHl] in df mf * => H. by rewrite !big_ord0 dhomog1. rewrite !big_ord_recr /=; apply dhomogM; last exact: H. by apply: IHl => i; exact: H. 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