Infinite series is summable iff 'tail' of series is summable

Stream: Is there code for X?

[Mark Gerads]

Do we have
lemma summable_iff_summable_tail {f : ℕ → ℂ}: ∀ (k : ℕ), (summable f ↔ summable (λ(n:ℕ),f (n+k))):=
or a generalization thereof?
If not, perhaps
lemma summable_iff_summable_tail_step {f : ℕ → ℂ}: (summable f ↔ summable (λ(n:ℕ),f (n+1))):=
, on which induction could be done to get the former?

[Heather Macbeth]

Maybe docs#summable_nat_add_iff

[Yaël Dillies]

I think you can more generally replace n + k to something using cofinite.

[Yury G. Kudryashov]

Probably you need a map f such that map f cofinite = cofinite (or in case of nat, map f at_top = at_top).