proposition: Lemma symbp_basis : [char R] =i pred0 -> basis_of fullv symbp.
proof: Proof. Proof using Hd. move=> Hchar. rewrite basisEdim size_map size_tuple dim_homsym leqnn andbT. rewrite -(span_basis symbh_basis). apply/span_subvP => s /mapP[/= la]; rewrite !mem_enum => _ ->{s}. pose co := fun (n : nat) (l : 'P_n) => (permcent.zcard l)%:R^-1 : R. have -> : 'hh[la] = \sum_(mu : 'P_d) coeff_prodgen co la mu *: 'hp[mu] :> HSF. apply val_inj; rewrite /= linear_sum /=. by rewrite (prod_prodgen (fun n => symh_to_symp n0 n Hchar)). 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