proposition: Fact homsymdotr_is_scalar p : scalar (homsymdotr p).
proof: Proof. move=> a /= u v. rewrite mulr_sumr /= -big_split; apply: eq_bigr => x _ /=. rewrite linearD linearZ /= mulrDr mulrDl !mulrA; congr (_ + _). by rewrite [_ * a]mulrC -!mulrA. 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