simp only [hn, eval₂_one, eval₂_X_pow, eval₂_sub, sub_self]
case right
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
⊢ eval₂ (algebraMap ℤ K) x (X ^ n - 1) = 0
no goals