proposition: Lemma homsymdotE p q : '[ p | q ] = \sum_(la : 'P_d) (zcard la)%:R * (coord 'hp (enum_rank la) p) * (coord 'hp (enum_rank la) q)^*.
proof: Proof. rewrite /homsymdot [RHS](reindex _ (onW_bij _ (@enum_val_bij _))) /=. by apply/eq_bigr => i _; rewrite enum_valK. 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