Theorems · Theorem · sequences and series

Summable.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}, Summable f → Summable g → Summable fun i => f i.1 * g i.2

Let R be a nonarchimedean ring. If functions f : α → R and g : β → R are summable, then so is fun i : α × β ↦ f i.1 * g i.2.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingUniformSpaceIsUniformAddGroupNonarchimedeanRing