Theorems · Theorem · sequences and series

tsum_mul_tsum_of_nonarchimedean

∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R]
  [NonarchimedeanRing R] [T0Space R] {f : α → R} {g : β → R},
  Summable f → Summable g → (∑' (i : α), f i) * ∑' (i : β), g i = ∑' (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

RingUniformSpaceIsUniformAddGroupNonarchimedeanRingT0Space