proposition: Lemma scaler_sumr a I r (P : pred I) (F : I -> V) : a *: (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) a *: F i.
proof: Proof. exact: big_endo (scalerDr a) (scaler0 a) I r P F. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)