Theorems · Theorem · complex analysis

RCLike.re_tsum

∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} [L.NeBot] {f : α → 𝕜},
  Summable f L → RCLike.re (∑'[L] (a : α), f a) = ∑'[L] (a : α), RCLike.re (f a)

Defined in

Mathlib.Analysis.Complex.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeSummationFilter.NeBot