K : Type u_1
inst✝ : Field K
n : ℕ
⊢ ∀ (j : K), j ∈ primitiveRoots n K → Splits (RingHom.id K) (X - ↑C j)
K : Type u_1
inst✝ : Field K
n : ℕ
⊢ Splits (RingHom.id K) (cyclotomic' n K)
apply splits_prod (RingHom.id K)
K : Type u_1
inst✝ : Field K
n : ℕ
z : K
a✝ : z ∈ primitiveRoots n K
⊢ Splits (RingHom.id K) (X - ↑C z)
K : Type u_1
inst✝ : Field K
n : ℕ
⊢ ∀ (j : K), j ∈ primitiveRoots n K → Splits (RingHom.id K) (X - ↑C j)
intro z _
no goals
K : Type u_1
inst✝ : Field K
n : ℕ
z : K
a✝ : z ∈ primitiveRoots n K
⊢ Splits (RingHom.id K) (X - ↑C z)
simp only [splits_X_sub_C (RingHom.id K)]