Infinite sums and products in topological fields

Lemmas on topological sums in rings with a strictly multiplicative norm, of which normed fields are the most familiar examples.

theorem HasProd.norm {α : Type u_1} {E : Type u_2} [SeminormedCommRing E] [NormMulClass E] [NormOneClass E] {f : α → E} {x : E} (hfx : HasProd f x) : HasProd (fun (x : α) => ‖f x‖) ‖x‖

theorem Multipliable.norm {α : Type u_1} {E : Type u_2} [SeminormedCommRing E] [NormMulClass E] [NormOneClass E] {f : α → E} (hf : Multipliable f) : Multipliable fun (x : α) => ‖f x‖

theorem Multipliable.norm_tprod {α : Type u_1} {E : Type u_2} [SeminormedCommRing E] [NormMulClass E] [NormOneClass E] {f : α → E} (hf : Multipliable f) : ‖∏' (i : α), f i‖ = ∏' (i : α), ‖f i‖

@[deprecated Multipliable.norm_tprod (since := "2025-04-12")]

theorem norm_tprod {α : Type u_1} {E : Type u_2} [SeminormedCommRing E] [NormMulClass E] [NormOneClass E] {f : α → E} (hf : Multipliable f) : ‖∏' (i : α), f i‖ = ∏' (i : α), ‖f i‖

Alias of Multipliable.norm_tprod.