obtain ⟨i, ⟨_, rfl⟩⟩ := hζ.eq_pow_of_pow_eq_one ((Polynomial.mem_nthRootsFinset n.2).1 hη) n.2
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
η : A
hη : η ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) η = 1
case intro.intro
p : ℕ+
K : Type ?u.247041
inst✝⁴ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ+
ζ : A
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hη : ζ ^ i ∈ nthRootsFinset (↑n) A
⊢ (Ideal.Quotient.mk (Ideal.span {ζ - 1})) (ζ ^ i) = 1