α : Type ?u.36846
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a => ↑(f (a + k))) ↔ Summable fun a => ↑(f a)
α : Type ?u.36846
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun i => f (i + k)) ↔ Summable f
rw [← summable_coe, ← summable_coe]
no goals
α : Type ?u.36846
f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun a => ↑(f (a + k))) ↔ Summable fun a => ↑(f a)
exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k