M : Type ?u.2777832
N : Type ?u.2777835
G : Type ?u.2777838
R : Type u_1
S : Type ?u.2777844
F : Type ?u.2777847
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
⊢ (1 - ζ) * ∑ i in range k, ζ ^ i = 0
M : Type ?u.2777832
N : Type ?u.2777835
G : Type ?u.2777838
R : Type u_1
S : Type ?u.2777844
F : Type ?u.2777847
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
⊢ ∑ i in range k, ζ ^ i = 0
refine' eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero_of_ne (hζ.ne_one hk).symm) _
no goals
M : Type ?u.2777832
N : Type ?u.2777835
G : Type ?u.2777838
R : Type u_1
S : Type ?u.2777844
F : Type ?u.2777847
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
⊢ (1 - ζ) * ∑ i in range k, ζ ^ i = 0
rw [mul_neg_geom_sum, hζ.pow_eq_one, sub_self]