proposition: Theorem homsymdotss la mu : '[ 'hsC[la] | 'hsC[mu] ] = (la == mu)%:R.
proof: Proof. Proof using Hd. have to_p (nu : 'P_d) : 'hsC[nu] \in span 'hp. by rewrite (span_basis (symbp_basis Hd _)) // memvf. rewrite (coord_span (to_p la)) (coord_span (to_p mu)). transitivity (\sum_i (coord 'hp i 'hsC[la]) * (zcard (enum_val i))%:R * (coord 'hp i 'hsC[mu])); first last. rewrite (reindex _ (onW_bij _ (@enum_rank_bij _))) /=. rewrite -coord_zsymspsp //; apply eq_bigr => /= nu _. by rewrite enum_rankK mulrA. rewrite homsymdot_suml; apply eq_bigr => /= l _. rewrite homsymdotZl homsymdot_sumr -mulrA; congr (_ * _). transitivity (\sum_(i < #|{:'P_d}|) (coord 'hp i 'hsC[mu])^* * (zcard (enum_val l))%:R * (i == l)%:R). apply: eq_bigr => i _; rewrite homsymdotZr -mulrA; congr (_ * _). rewrite !(nth_map inh _ (fun l => 'hp[l])) -?cardE ?ltn_ord //. by rewrite -!enum_val_nth homsymdotpp // (inj_eq enum_val_inj) eq_sym. rewrite (bigD1 l) //= big1 ?addr0; last by move=> m /negbTE ->; rewrite mulr0. rewrite eq_refl mulr1 mulrC; congr (_ * _). by rewrite -coord_map_homsym ?map_homsymbp ?symbp_basis // map_homsyms. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent