n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Monic (map (Int.castRingHom R) (cyclotomic n ℤ))
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Monic (cyclotomic n R)
rw [← map_cyclotomic_int]
no goals
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Monic (map (Int.castRingHom R) (cyclotomic n ℤ))
exact (int_cyclotomic_spec n).2.2.map _