Theorem: NeedZeroCoeff (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
f : ℕ → ℂ
n : ℕ+
⊢ ∑' (k : ℕ), f (↑n * k) = ∑' (k : ℕ), if ↑↑n ∣ ↑k then f k else 0
Tactic:
exact TsumMulIte _
State after:
no goals