proposition: Lemma symbh_basis : basis_of fullv symbh.
proof: Proof. Proof using Hd. rewrite basisEdim size_map size_tuple dim_homsym leqnn andbT. rewrite -(span_basis symbe_basis). apply/span_subvP => s /mapP[/= la]; rewrite !mem_enum => _ ->{s}. have -> : 'he[la] = \sum_(mu : 'P_d) coeff_prodgen (fun d (la : 'P_d) => (-1)^+(d - size la) * (perm_partn la)%:R) la mu *: 'hh[mu] :> HSF. by apply val_inj; rewrite /= linear_sum /= (prod_prodgen (syme_to_symh n0 R)). rewrite span_def; apply memv_suml => mu _; apply memvZ. rewrite big_map (bigD1_seq mu) /= ?mem_enum ?inE ?enum_uniq //. rewrite -[X in X \in _]addr0. by apply memv_add; [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