Theorem: RuesDiffHasDeriv (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
m : ℤ
z : ℂ
⊢ HasDerivAt (RuesDiff n m) (RuesDiff n (m + 1) z) z
Tactic:
sorry
State after:
no goals