Theorem: CyclotomicIntegers.sum_zeta_pow (FltRegular/NumberTheory/CyclotomicRing.lean)

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

State before:
p : ℕ
hpri : Fact p.Prime
⊢ ∑ i ∈ Finset.range p, zeta p ^ i = (aeval (zeta p)) (cyclotomic p ℤ)
Tactic:
simp [Polynomial.cyclotomic_prime ℤ p]
State after:
no goals