Theorem: EqualsNthDerivRuesDiffSum (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
f : ℂ → ℂ
n : ℕ+
⊢ f = iteratedDeriv (↑n) f ↔ f = ∑ k ∈ range ↑n, (fun z => iteratedDeriv k f 0) * RuesDiff n (-↑k)
Tactic:
sorry
State after:
no goals