chore(topology/algebra/infinite_sum): relax the requirements on `has_…

…sum.smul` (#8312)
leanprover-community · Jul 16, 2021 · 35a8d93 · 35a8d93
1 parent 162221f
commit 35a8d93
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean
@@ -735,9 +735,9 @@ end topological_semiring
 
 section has_continuous_smul
 variables {R : Type*}
-[semiring R] [topological_space R]
+[monoid R] [topological_space R]
 [topological_space α] [add_comm_monoid α]
-[module R α] [has_continuous_smul R α]
+[distrib_mul_action R α] [has_continuous_smul R α]
 {f : β → α}
 
 lemma has_sum.smul {a : α} {r : R} (hf : has_sum f a) : has_sum (λ z, r • f z) (r • a) :=