proposition: Lemma symbe_basis : basis_of fullv symbe.
proof: Proof. Proof using Hd. rewrite basisEdim size_map size_tuple dim_homsym leqnn andbT. apply/subvP => /= p _; rewrite span_def big_map. have:= sym_fundamental_homog (sympolP p) (homsym_is_dhomog p). move=> [t [Hp /dhomogP Hhomt]]. have {Hp} -> : p = \sum_(m <- msupp t) t@_m *: in_homsym d ('X_[m] \mPo E). apply val_inj; apply val_inj; rewrite /= -{1}Hp {1}(mpolyE t) {Hp}. rewrite !linear_sum /=; apply eq_big_seq => m /Hhomt /= Hm. rewrite !linearZ /=; congr (_ *: _). by rewrite in_homsym_comp_symbe /= comp_symbe /=. rewrite big_seq; apply memv_suml => m Hm; apply memvZ. rewrite (in_homsym_comp_symbe (Hhomt m Hm)). move: (intpartn_of_mon _) => {m Hm} la. rewrite (bigD1_seq la) /= ?mem_enum ?inE ?enum_uniq //. rewrite -[X in X \in _]addr0. apply memv_add; first exact: memv_line. exact: mem0v. 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