case pos
α : Type u_1
β : Type u_2
γ : Type ?u.442177
δ : Type ?u.442180
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : Summable f
⊢ (∑' (b : β), -f b) = -∑' (b : β), f b

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.442177
δ : Type ?u.442180
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
⊢ (∑' (b : β), -f b) = -∑' (b : β), f b
α : Type u_1
β : Type u_2
γ : Type ?u.442177
δ : Type ?u.442180
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
⊢ (∑' (b : β), -f b) = -∑' (b : β), f b
by_cases hf : Summable f
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.442177
δ : Type ?u.442180
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : Summable f
⊢ (∑' (b : β), -f b) = -∑' (b : β), f b
exact hf.hasSum.neg.tsum_eq
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.442177
δ : Type ?u.442180
inst✝³ : AddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
⊢ (∑' (b : β), -f b) = -∑' (b : β), f b
simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt Summable.of_neg hf)]