α : Type u_1
β : Type ?u.482840
γ : Type ?u.482843
δ : Type ?u.482846
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f : ℤ → α
hpos : HasSum (fun n => f (↑n + 1)) a
hneg : HasSum (fun n => f (-↑(Nat.succ n))) b
g : ℕ → α
hg : HasSum (fun k => g (k + 1)) a
⊢ HasSum g (a + g 0)
α : Type u_1
β : Type ?u.482840
γ : Type ?u.482843
δ : Type ?u.482846
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a a₁ a₂ b : α
f : ℤ → α
hpos : HasSum (fun n => f (↑n + 1)) a
hneg : HasSum (fun n => f (-↑(Nat.succ n))) b
⊢ ∀ (g : ℕ → α), HasSum (fun k => g (k + 1)) a → HasSum g (a + g 0)
intro g hg
no goals
α : Type u_1
β : Type ?u.482840
γ : Type ?u.482843
δ : Type ?u.482846
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g✝ : β → α
a a₁ a₂ b : α
f : ℤ → α
hpos : HasSum (fun n => f (↑n + 1)) a
hneg : HasSum (fun n => f (-↑(Nat.succ n))) b
g : ℕ → α
hg : HasSum (fun k => g (k + 1)) a
⊢ HasSum g (a + g 0)
simpa using (hasSum_nat_add_iff _).mp hg