proposition: Lemma symh_syms_int mu : 'h[mu] = \sum_(la : 'P_d) 'K(la, mu) *: 's[la] :> SF.
proof: Proof. case: mu => [mu Hmu] /=; rewrite /prod_symh /prod_gen /=. elim: mu d Hmu => [|m mu IHmu] deg. rewrite big_nil => /andP[/eqP /= /esym Hd _]. symmetry; subst deg; rewrite (big_pred1 (rowpartn 0)); first last. by move=> i; symmetry; apply/eqP/val_inj; rewrite /= intpartn0. by rewrite syms0 -rowpartn0E Kostka_diag scale1r. move=> /=/andP[/eqP/esym Hdeg /andP[_ Hpart]]. rewrite big_cons /= (IHmu (sumn mu)) /= ?eq_refl ?Hpart //. under [RHS]eq_bigr do rewrite Kostka_ind ?Hdeg // natr_sum scaler_suml. rewrite mulr_sumr [RHS](exchange_big_dep predT) //=. apply eq_bigr => la _. rewrite -scalerAr -scaler_sumr mulrC syms_symhM; congr (_ *: _). rewrite addnC in Hdeg. rewrite (reindex _ (onW_bij _ (cast_intpartn_bij Hdeg))) /=. apply eq_big => [nu | nu _]. - by case: nu => nu /= Hnu; rewrite cast_intpartnE /=. - by apply val_inj; rewrite /= Schur_cast. 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