Theorems · Theorem · complex analysis

RCLike.hasSum_iff

∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {L : SummationFilter α} (f : α → 𝕜) (c : 𝕜),
  HasSum f c L ↔ HasSum (fun x => RCLike.re (f x)) (RCLike.re c) L ∧ HasSum (fun x => RCLike.im (f x)) (RCLike.im c) L

Defined in

Mathlib.Analysis.Complex.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLike