Theorems · Theorem · functional analysis

HasSum.smul_eq

∀ {ι : Type u_5} {κ : Type u_6} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace M] [T3Space M] [ContinuousAdd M]
  [ContinuousSMul R M] {f : ι → R} {g : κ → M} {s : R} {t u : M},
  HasSum f s → HasSum g t → HasSum (fun x => f x.1 • g x.2) u → s • t = u

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Module

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleTopologicalSpaceTopologicalSpaceT3SpaceContinuousAddContinuousSMul