proposition: Lemma symbs_basis : basis_of fullv symbs.
proof: Proof. Proof using Hd. rewrite basisEdim size_map size_tuple dim_homsym leqnn andbT. rewrite -(span_basis symbm_basis). apply/span_subvP => s /mapP[/= la]; rewrite !mem_enum => _ ->{s}. have -> : 'hm[la] = \sum_(mu : 'P_d) 'K^-1(la, mu) *: 'hs[mu] :> HSF. by apply val_inj; rewrite /= (symm_syms _ _ la) !linear_sum. 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