no goals
R : Type u
S : Type v
T : Type w
a b : R
n✝ : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
n : ℕ
h : 0 < n
x : R
⊢ x ∈ nthRootsFinset n R ↔ x ^ n = 1
rw [nthRootsFinset, mem_toFinset, mem_nthRoots h]