Theorem: RuesDiffSummable (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
m : ℤ
z : ℂ
⊢ Summable fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0
Tactic:
sorry
State after:
no goals