α : Type u_1
β : Type ?u.450378
γ : Type ?u.450381
δ : Type ?u.450384
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum (fun x => f ↑x) a
α : Type u_1
β : Type ?u.450378
γ : Type ?u.450381
δ : Type ?u.450384
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i in range k, f i)
refine' Iff.trans _ (range k).hasSum_compl_iff
α : Type u_1
β : Type ?u.450378
γ : Type ?u.450381
δ : Type ?u.450384
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum ((fun x => f ↑x) ∘ ↑(notMemRangeEquiv k).symm) a
α : Type u_1
β : Type ?u.450378
γ : Type ?u.450381
δ : Type ?u.450384
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum (fun x => f ↑x) a
rw [← (notMemRangeEquiv k).symm.hasSum_iff]
no goals
α : Type u_1
β : Type ?u.450378
γ : Type ?u.450381
δ : Type ?u.450384
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalAddGroup α
f✝ g : β → α
a✝ a₁ a₂ : α
f : ℕ → α
k : ℕ
a : α
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum ((fun x => f ↑x) ∘ ↑(notMemRangeEquiv k).symm) a
rfl