nth_rw 1 [this]
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
this : ζ = (ζ ^ j) ^ m
⊢ 1 - ζ = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i
case h
n✝ : ℕ+
K : Type u
L : Type v
A : Type w
B : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : IsCyclotomicExtension {n✝} A B
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
n : ℕ
ζ : A
hζ : IsPrimitiveRoot ζ n
j : ℕ
hj : j.Coprime n
hn' : n ≠ 0
hn : 1 < n
m : ℕ
hm : j * m % n = 1
this : ζ = (ζ ^ j) ^ m
⊢ 1 - (ζ ^ j) ^ m = (1 - ζ ^ j) * ∑ i ∈ range m, (ζ ^ j) ^ i