simp [IsPrimitiveRoot.one_right_iff.mp hζ]
case inr.inl
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
ζ : A
j : ℕ
hζ : IsPrimitiveRoot ζ 1
hj : j.Coprime 1
hn' : 1 ≠ 0
⊢ 1 - ζ ^ j ∣ 1 - ζ
no goals