rw [← AdjoinRoot.aeval_root (Polynomial.cyclotomic p ℤ), ← zeta]
p : ℕ
hpri : Fact p.Prime
⊢ ∑ i ∈ Finset.range p, zeta p ^ i = 0
p : ℕ
hpri : Fact p.Prime
⊢ ∑ i ∈ Finset.range p, zeta p ^ i = (aeval (zeta p)) (cyclotomic p ℤ)