Theorems · Theorem · sequences and series

HasSum.mul_of_nonarchimedean

∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R]
  [NonarchimedeanRing R] {f : α → R} {g : β → R} {a b : R},
  HasSum f a → HasSum g b → HasSum (fun i => f i.1 * g i.2) (a * b)

Let R be a nonarchimedean ring, let f : α → R be a function that sums to a : R, and let g : β → R be a function that sums to b : R. Then fun i : α × β ↦ f i.1 * g i.2 sums to a * b.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Cited by

2 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingUniformSpaceIsUniformAddGroupNonarchimedeanRing