case pos
α : Type u_1
β : Type u_2
γ : Type ?u.819769
δ : Type ?u.819772
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
hf : Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.819769
δ : Type ?u.819772
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
hf : ¬Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)
α : Type u_1
β : Type u_2
γ : Type ?u.819769
δ : Type ?u.819772
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)
by_cases hf : Summable f
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.819769
δ : Type ?u.819772
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
hf : Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)
exact hf.hasSum.star.tsum_eq.symm
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.819769
δ : Type ?u.819772
inst✝⁴ : AddCommMonoid α
inst✝³ : TopologicalSpace α
inst✝² : StarAddMonoid α
inst✝¹ : ContinuousStar α
f : β → α
a : α
inst✝ : T2Space α
hf : ¬Summable f
⊢ star (∑' (b : β), f b) = ∑' (b : β), star (f b)
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt Summable.ofStar hf),
  star_zero]