Infinite sums and products in topological fields

Lemmas on topological sums in fields (as opposed to groups).

theorem HasProd.norm {α : Type u_1} {E : Type u_2} [NormedField 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} [NormedField E] {f : α → E} (hf : Multipliable f) : Multipliable fun (x : α) => ‖f x‖

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