Show a tsum is Summable and has a derivative

Stream: Is there code for X?

[Mark Andrew Gerads]

import Mathlib

-- (RuesDiff n m) is the mth derivative of (Rues n)
noncomputable
def RuesDiff (n : ℕ+) (m : ℤ) (z : ℂ) : ℂ :=
  tsum (λ (k : ℕ) => if ↑↑n ∣ (↑k + m) then z ^ k / k.factorial else 0)

lemma RuesDiffSummable (n : ℕ+) (m : ℤ) (z : ℂ) : Summable (λ (k : ℕ) => if ↑↑n ∣ (↑k + m) then z ^ k / k.factorial else 0) := by
  sorry

lemma RuesDiffHasDeriv (n : ℕ+) (m : ℤ) (z : ℂ) : HasDerivAt (RuesDiff n m) (RuesDiff n (m + 1) z) z := by
  sorry

I am vaguely aware that I should use code like this:

def RuesDiffSeries (n : ℕ+) (m : ℤ) : FormalMultilinearSeries ℂ ℂ ℂ :=

because I got some help with related Lean 3 code.
Unfortunately, I never fully understood the code, and I have had trouble every time I tried to port it to Lean 4.
It doesn't help that I haven't been able to get the Lean 3 Server working recently, making understanding Lean 3 code more difficult.
Please write simple understandable code, if possible, and thanks to all who help.

[Aaron Liu]

I have

lemma RuesDiffSummable (n : ℕ+) (m : ℤ) (z : ℂ) : Summable (λ (k : ℕ) => if ↑↑n ∣ (↑k + m) then z ^ k / k.factorial else 0) := by
  apply Summable.of_norm_bounded _ <| Real.summable_pow_div_factorial (norm z)
  · intro N
    split
    · simp
    · rw [norm_zero, Complex.norm_eq_abs]
      positivity

[Mark Andrew Gerads]

I am grateful for the Summable proof.
Someone, please help with the HasDerivAt proof.