feat(algebra/module): sum_smul' (for semimodules) (#1752)

* feat(algebra/module): sum_smul' (for semimodules)

* adding docstring

* use `classical` tactic

* moving ' name to the weaker theorem

Author: kbuzzard

src/algebra/big_operators.lean

@@ -428,10 +428,10 @@ end comm_monoid
 
 attribute [to_additive] prod_hom
 
-lemma sum_smul [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
+lemma sum_smul' [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
   s.sum (λ x, add_monoid.smul n (f x)) = add_monoid.smul n (s.sum f) :=
 @prod_pow _ (multiplicative β) _ _ _ _
-attribute [to_additive sum_smul] prod_pow
+attribute [to_additive sum_smul'] prod_pow
 
 @[simp] lemma sum_const [add_comm_monoid β] (b : β) :
   s.sum (λ a, b) = add_monoid.smul s.card b :=

src/algebra/module.lean

@@ -54,6 +54,13 @@ instance smul.is_add_monoid_hom {r : α} : is_add_monoid_hom (λ x : β, r • x
 lemma semimodule.eq_zero_of_zero_eq_one (zero_eq_one : (0 : α) = 1) : x = 0 :=
 by rw [←one_smul α x, ←zero_eq_one, zero_smul]
 
+/-- R-linearity of finite sums of elements of an R-semimodule. -/
+lemma finset.sum_smul {α : Type*} {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M]
+  [semimodule R M] (s : finset α) (r : R) (f : α → M) :
+    finset.sum s (λ (x : α), (r • (f x))) = r • (finset.sum s f) :=
+by classical; exact
+finset.induction_on s (by simp) (by simp [_root_.smul_add] {contextual := tt})
+
 end semimodule
 
 section prio