proposition: Lemma scaler_suml v I r (P : pred I) F : (\sum_(i <- r | P i) F i) *: v = \sum_(i <- r | P i) F i *: v.
proof: Proof. exact: (big_morph _ (scalerDl v) (scale0r v)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)