refine' ⟨X ^ n - 1, _⟩
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ IsIntegral ℤ x
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
⊢ (X ^ n - 1).Monic ∧ eval₂ (algebraMap ℤ K) x (X ^ n - 1) = 0