case pos
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → ℝ
h : Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

case neg
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → ℝ
h : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → ℝ
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
by_cases h : Summable f
no goals
case pos
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → ℝ
h : Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
exact ContinuousLinearMap.map_tsum ofRealClm h
no goals
case neg
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → ℝ
h : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
rw [tsum_eq_zero_of_not_summable h,
  tsum_eq_zero_of_not_summable ((summable_ofReal _).not.mpr h), ofReal_zero]