proposition: Lemma coord_zsymspsp (la mu : 'P_d) : (\sum_nu (coord 'hp (enum_rank nu) 'hsC[la]) * ((zcard nu)%:R * coord 'hp (enum_rank nu) 'hsC[mu])) = (la == mu)%:R.
proof: Proof. Proof using Hd. pose matsp : 'M[algC]_#|{:'P_d}| := \matrix_(i, j < #|{:'P_d}|) (coord 'hp i 'hsC[enum_val j]). pose matzsp : 'M[algC]_#|{:'P_d}| := \matrix_(i, j < #|{:'P_d}|) ((zcard (enum_val j))%:R * (coord 'hp j 'hsC[enum_val i])). have: matsp *m matzsp = 1%:M. apply/matrixP => i j /=. rewrite /matsp /matzsp /= !mxE. rewrite (reindex _ (onW_bij _ (@enum_rank_bij _))) /=. rewrite -(inj_eq (@enum_val_inj _ _)) /= -coord_zsympsps //. apply eq_bigr => /= nu _. by rewrite !mxE !enum_valK !enum_rankK. move=> /mulmx1C/matrixP/(_ (enum_rank mu) (enum_rank la)). rewrite /matsp /matzsp /= !mxE. rewrite (inj_eq (@enum_rank_inj _)) eq_sym => <-. rewrite (reindex _ (onW_bij _ (@enum_rank_bij _))) /=. apply eq_bigr => /= nu _. by rewrite !mxE !enum_rankK mulrC. 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