proposition: Lemma symh_to_symp_prod_partsum n : [char R] =i pred0 -> 'h_n = \sum_(c : intcompn n) \Pi c *: \prod_(i <- c) 'p_i :> SF.
proof: Proof. Proof using. rewrite -big_enum /= charf0P => Hchar. rewrite -[RHS](big_map (@cnval n) xpredT (fun c : seq nat => \Pi c *: \prod_(i <- c) 'p_i)). rewrite enum_intcompnE. have [m/ltnW] := ubnP n; elim: m => [| m IHm] in n *. rewrite leqn0 => /eqP ->. by rewrite big_seq1 big_nil symh0 /= invr1 scale1r. rewrite leq_eqVlt => /orP[/eqP Hm |]; last by rewrite ltnS; exact: IHm. rewrite enum_compnE Hm // -Hm big_flatten /=. have Hn : (n%:R : R) != 0 by rewrite Hchar Hm. apply (scalerI Hn); rewrite Newton_symh1 /index_iota subn1 /=. rewrite scaler_sumr big_map; apply eq_big_seq => i. rewrite mem_iota add1n ltnS => /andP[Hi Hin]. rewrite big_map big_seq. rewrite (eq_bigr (fun c => (n%:R^-1 *: 'p_i) * (\Pi c *: \prod_(j <- c) 'p_j))); first last. move=> s; rewrite -enum_compnP /is_comp_of_n /= => /andP[/eqP -> _]. rewrite subnKC // big_cons scalerAr. by rewrite natrM invfM -!scalerAr -scalerAl scalerA mulrC. rewrite -big_seq -mulr_sumr {}IHm; first last. by rewrite leq_subLR Hm -(add1n m) leq_add2r. by rewrite -scalerAl scalerA divff // scale1r. 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