no goals
M : Type ?u.2780127
N : Type ?u.2780130
G : Type ?u.2780133
R : Type u_1
S : Type ?u.2780139
F : Type ?u.2780142
inst✝⁴ : CommMonoid M
inst✝³ : CommMonoid N
inst✝² : DivisionCommMonoid G
k l : ℕ
inst✝¹ : CommRing R
ζ✝ : Rˣ
h : IsPrimitiveRoot ζ✝ k
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ ζ ^ Nat.pred k = -∑ i in range (Nat.pred k), ζ ^ i
rw [eq_neg_iff_add_eq_zero, add_comm, ← sum_range_succ, ← Nat.succ_eq_add_one,
  Nat.succ_pred_eq_of_pos (pos_of_gt hk), hζ.geom_sum_eq_zero hk]