proposition: Lemma symbm_free : free symbm.
proof: Proof. Proof using Hd. apply/freeP => co. rewrite (reindex _ (onW_bij _ (@enum_rank_bij 'P_d))) /=. rewrite (eq_bigr (fun la : 'P_d => (co (enum_rank la)) *: 'hm[la])); first last. move=> la _; rewrite (nth_map (rowpartn _)) /= -?cardE ?ltn_ord //. by rewrite -?enum_val_nth enum_rankK. move => /(congr1 val). rewrite /= linear_sum /= => /symm_unique0 H i. rewrite -(enum_valK i); apply H. apply: (leq_trans _ Hd). rewrite -[X in (_ <= X)%N](sumn_intpartn (enum_val i)). exact: size_part. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg matrix vector ssrnum algC archimedean) mathcomp(fingroup perm) mathcomp(ssrcomplements freeg mpoly) tools sorted ordtype permuted partition permcent antisym Schur_mpoly Schur_altdef sympoly