α : Type u_2
β : Type u_1
γ : Type ?u.448190
δ : Type ?u.448193
inst✝⁴ : AddCommGroup α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Summable f
b : β
⊢ (∑' (n : β), f n) = f b + ((∑' (b : β), f b) - f b)
α : Type u_2
β : Type u_1
γ : Type ?u.448190
δ : Type ?u.448193
inst✝⁴ : AddCommGroup α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Summable f
b : β
⊢ (∑' (n : β), f n) = f b + ∑' (n : β), if n = b then 0 else f n
rw [(hasSum_ite_sub_hasSum hf.hasSum b).tsum_eq]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.448190
δ : Type ?u.448193
inst✝⁴ : AddCommGroup α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalAddGroup α
f g : β → α
a a₁ a₂ : α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Summable f
b : β
⊢ (∑' (n : β), f n) = f b + ((∑' (b : β), f b) - f b)
exact (add_sub_cancel'_right _ _).symm