Theorem: RuesDiffZ0EqualsIte (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
m : ℤ
⊢ RuesDiff n m 0 = if ↑↑n ∣ m then 1 else 0
Tactic:
sorry
State after:
no goals