proposition: Lemma basis_homsym : [set p : 'P_d | (size p <= n)%N] =i {:'P_d}.
proof: Proof. Proof using Hd. move=> la. rewrite !inE; apply: (leq_trans _ Hd). by rewrite -[X in (_ <= X)%N](sumn_intpartn la); apply: 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