proposition: Lemma homsymdotpp (Hd : (d <= n)%N) la mu : '[ 'hp[la] | 'hp[mu] ] = (zcard la)%:R * (la == mu)%:R.
proof: Proof. rewrite homsymdotE (bigD1 mu) //= big1 ?addr0 => [| nu /negbTE Hneq]. - rewrite !(coord_symbp Hd) // eq_refl /= conjC1 mulr1. by case: eqP => [-> //| _]; rewrite !mulr0. - by rewrite !(coord_symbp Hd) // [mu == nu]eq_sym Hneq conjC0 mulr0. 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