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

State before:
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) = -∑ i : Fin (p - 1), zeta p ^ ↑i
Tactic:
rw [eq_neg_iff_add_eq_zero]
State after:
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = 0

State before:
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = 0
Tactic:
convert CyclotomicIntegers.sum_zeta_pow p
State after:
case h.e'_2
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = ∑ i ∈ Finset.range p, zeta p ^ i

State before:
case h.e'_2
p : ℕ
hpri : Fact p.Prime
⊢ zeta p ^ (p - 1) + ∑ i : Fin (p - 1), zeta p ^ ↑i = ∑ i ∈ Finset.range p, zeta p ^ i
Tactic:
conv_rhs => enter [1]; rw [← tsub_add_cancel_of_le hpri.out.one_lt.le]
State after:
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

State before:
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
Tactic:
rw [Finset.sum_range_succ, add_comm, Fin.sum_univ_eq_sum_range]
State after:
no goals