∀ (n : ℕ),
  Polynomial.map (Int.castRingHom ℂ) (Polynomial.cyclotomic n ℤ) = Polynomial.cyclotomic' n ℂ ∧
    (Polynomial.cyclotomic n ℤ).degree = (Polynomial.cyclotomic' n ℂ).degree ∧ (Polynomial.cyclotomic n ℤ).Monic