obtain ⟨i, ⟨hi, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset hp.pos).1 hη₁) hp.pos
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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p A
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
e : η₁ ≠ η₂
⊢ Associated (ζ - 1) (η₁ - η₂)
case intro.intro
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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
p : ℕ
hp : p.Prime
ζ : A
hζ : IsPrimitiveRoot ζ p
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p A
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ nthRootsFinset p A
e : ζ ^ i ≠ η₂
⊢ Associated (ζ - 1) (ζ ^ i - η₂)