no goals
K : Type u_1
inst✝ : Field K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ Splits (RingHom.id K) (X ^ n - ↑C 1)
rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots h, natDegree_X_pow_sub_C]