rw [Finset.sum_range_succ, add_comm, Fin.sum_univ_eq_sum_range]
case h.e'_2
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = ∑ i ∈ Finset.range (p - 1 + 1), zeta p ^ i
no goals