n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n ℤ ∣ X ^ n - 1
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n R ∣ X ^ n - 1
suffices cyclotomic n ℤ ∣ X ^ n - 1 by
  simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
    Polynomial.map_X] using map_dvd (Int.castRingHom R) this
case inl
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 ℤ ∣ X ^ 0 - 1

case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ X ^ n - 1
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic n ℤ ∣ X ^ n - 1
rcases n.eq_zero_or_pos with (rfl | hn)
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ ∏ i in Nat.divisors n, cyclotomic i ℤ
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ X ^ n - 1
rw [← prod_cyclotomic_eq_X_pow_sub_one hn]
no goals
case inr
n : ℕ
R : Type u_1
inst✝ : Ring R
hn : n > 0
⊢ cyclotomic n ℤ ∣ ∏ i in Nat.divisors n, cyclotomic i ℤ
exact Finset.dvd_prod_of_mem _ (n.mem_divisors_self hn.ne')
no goals
n : ℕ
R : Type u_1
inst✝ : Ring R
this : cyclotomic n ℤ ∣ X ^ n - 1
⊢ cyclotomic n R ∣ X ^ n - 1
simpa only [map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
  Polynomial.map_X] using map_dvd (Int.castRingHom R) this
no goals
case inl
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 ℤ ∣ X ^ 0 - 1
simp