α : Type ?u.37164
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => ↑(f n)) (↑a + ∑ i in Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i in Finset.range k, f i)
α : Type ?u.37164
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i in Finset.range k, f i)
rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]
no goals
α : Type ?u.37164
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => ↑(f n)) (↑a + ∑ i in Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i in Finset.range k, f i)
norm_cast