proposition: Lemma homsymdot_suml p I r (P : pred I) (q : I -> HSF) : '[\sum_(i <- r | P i) q i | p] = \sum_(i <- r | P i) '[q i | p].
proof: Proof. by rewrite -!homsymdotrE linear_sum. 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