chore(algebra/module/basic): remove dependency on finiteness (#17764)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

src/algebra/module/basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
-import algebra.big_operators.basic
+
 import algebra.smul_with_zero
 import group_theory.group_action.group
 import tactic.abel
@@ -36,7 +36,6 @@ semimodule, module, vector space
 -/
 
 open function
-open_locale big_operators
 
 universes u v
 variables {α R k S M M₂ M₃ ι : Type*}
@@ -159,16 +158,6 @@ variables {R M}
 lemma module.eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0 :=
 by rw [←one_smul R x, ←zero_eq_one, zero_smul]
 
-lemma list.sum_smul {l : list R} {x : M} : l.sum • x = (l.map (λ r, r • x)).sum :=
-((smul_add_hom R M).flip x).map_list_sum l
-
-lemma multiset.sum_smul {l : multiset R} {x : M} : l.sum • x = (l.map (λ r, r • x)).sum :=
-((smul_add_hom R M).flip x).map_multiset_sum l
-
-lemma finset.sum_smul {f : ι → R} {s : finset ι} {x : M} :
-  (∑ i in s, f i) • x = (∑ i in s, (f i) • x) :=
-((smul_add_hom R M).flip x).map_sum f s
-
 @[simp] lemma smul_add_one_sub_smul {R : Type*} [ring R] [module R M]
   {r : R} {m : M} : r • m + (1 - r) • m = m :=
 by rw [← add_smul, add_sub_cancel'_right, one_smul]
@@ -643,5 +632,4 @@ by rw [nsmul_eq_mul, mul_one]
   m • (1 : R) = ↑m :=
 by rw [zsmul_eq_mul, mul_one]
 
-lemma finset.cast_card [comm_semiring R] (s : finset α) : (s.card : R) = ∑ a in s, 1 :=
-by rw [finset.sum_const, nat.smul_one_eq_coe]
+assert_not_exists multiset

src/algebra/module/big_operators.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
+-/
+
+import algebra.module.basic
+import algebra.big_operators.basic
+
+/-!
+# Finite sums over modules over a ring
+-/
+
+open_locale big_operators
+
+universes u v
+variables {α R k S M M₂ M₃ ι : Type*}
+section add_comm_monoid
+variables [semiring R] [add_comm_monoid M] [module R M] (r s : R) (x y : M)
+variables {R M}
+lemma list.sum_smul {l : list R} {x : M} : l.sum • x = (l.map (λ r, r • x)).sum :=
+((smul_add_hom R M).flip x).map_list_sum l
+
+lemma multiset.sum_smul {l : multiset R} {x : M} : l.sum • x = (l.map (λ r, r • x)).sum :=
+((smul_add_hom R M).flip x).map_multiset_sum l
+
+lemma finset.sum_smul {f : ι → R} {s : finset ι} {x : M} :
+  (∑ i in s, f i) • x = (∑ i in s, (f i) • x) :=
+((smul_add_hom R M).flip x).map_sum f s
+end add_comm_monoid
+
+lemma finset.cast_card [comm_semiring R] (s : finset α) : (s.card : R) = ∑ a in s, 1 :=
+by rw [finset.sum_const, nat.smul_one_eq_coe]

src/algebra/module/torsion.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pierre-Alexandre Bazin
 -/
 import algebra.direct_sum.module
+import algebra.module.big_operators
 import linear_algebra.isomorphisms
 import group_theory.torsion
 import ring_theory.coprime.ideal

src/algebra/monoid_algebra/basic.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
 -/
 import algebra.big_operators.finsupp
 import algebra.hom.non_unital_alg
+import algebra.module.big_operators
 import linear_algebra.finsupp
 
 /-!

src/algebra/order/rearrangement.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Mantas Bakšys. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mantas Bakšys
 -/
+import algebra.big_operators.basic
 import algebra.order.module
 import data.prod.lex
 import group_theory.perm.support

src/algebra/support.lean

@@ -5,6 +5,7 @@ Authors: Yury Kudryashov
 -/
 import order.conditionally_complete_lattice.basic
 import data.set.finite
+import algebra.big_operators.basic
 import algebra.group.prod
 import algebra.group.pi
 import algebra.module.basic

src/combinatorics/pigeonhole.lean

@@ -7,6 +7,7 @@ import data.nat.modeq
 import data.set.finite
 import algebra.big_operators.order
 import algebra.module.basic
+import algebra.module.big_operators
 
 /-!
 # Pigeonhole principles

src/linear_algebra/affine_space/combination.lean

@@ -5,6 +5,7 @@ Authors: Joseph Myers
 -/
 import algebra.invertible
 import algebra.indicator_function
+import algebra.module.big_operators
 import linear_algebra.affine_space.affine_map
 import linear_algebra.affine_space.affine_subspace
 import linear_algebra.finsupp

src/linear_algebra/dimension.lean

@@ -3,6 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johannes Hölzl, Sander Dahmen, Scott Morrison
 -/
+import algebra.module.big_operators
 import linear_algebra.dfinsupp
 import linear_algebra.invariant_basis_number
 import linear_algebra.isomorphisms

src/number_theory/arithmetic_function.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import algebra.big_operators.ring
+import algebra.module.big_operators
 import number_theory.divisors
 import data.nat.squarefree
 import data.nat.gcd.big_operators

src/ring_theory/algebra_tower.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.algebra.tower
 import algebra.invertible
+import algebra.module.big_operators
 import linear_algebra.basis
 
 /-!