feat(Topology/Algebra/InfiniteSum): use NormMulClass (#28756)

Prove `norm_tprod` and its cousins for any normed ring with a strictly multiplicative norm (not just fields).

Author: loefflerd

Mathlib/Topology/Algebra/InfiniteSum/Field.lean

@@ -4,19 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import Mathlib.Analysis.Normed.Group.Continuity
-import Mathlib.Analysis.Normed.Field.Basic
+import Mathlib.Analysis.Normed.Ring.Basic
 import Mathlib.Topology.Algebra.InfiniteSum.Defs
 
 /-!
 # Infinite sums and products in topological fields
 
-Lemmas on topological sums in fields (as opposed to groups).
+Lemmas on topological sums in rings with a strictly multiplicative norm, of which normed fields are
+the most familiar examples.
 -/
 
 
-section NormedField
+section NormMulClass
 
-variable {α E : Type*} [NormedField E] {f : α → E} {x : E}
+variable {α E : Type*} [SeminormedCommRing E] [NormMulClass E] [NormOneClass E]
+ {f : α → E} {x : E}
 
 nonrec theorem HasProd.norm (hfx : HasProd f x) : HasProd (‖f ·‖) ‖x‖ := by
   simp only [HasProd, ← norm_prod]
@@ -30,4 +32,4 @@ protected theorem Multipliable.norm_tprod (hf : Multipliable f) : ‖∏' i, f i
 
 @[deprecated (since := "2025-04-12")] alias norm_tprod := Multipliable.norm_tprod
 
-end NormedField
+end NormMulClass