R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d R ∣ ∑ i in range n, X ^ i
suffices cyclotomic d ℤ ∣ ∑ i in Finset.range n, X ^ i by
  simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
    map_dvd (Int.castRingHom R) this
case inl
R : Type u_1
inst✝ : Ring R
d : ℕ
hd : d ≠ 1
hdn : d ∣ 0
⊢ cyclotomic d ℤ ∣ ∑ i in range 0, X ^ i

case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
⊢ cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
rcases n.eq_zero_or_pos with (rfl | hn)
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
rw [← prod_cyclotomic_eq_geom_sum hn]
case inr.ha
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ d ∈ Finset.erase (Nat.divisors n) 1
case inr
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ cyclotomic d ℤ ∣ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ
apply Finset.dvd_prod_of_mem
no goals
case inr.ha
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
hn : n > 0
⊢ d ∈ Finset.erase (Nat.divisors n) 1
simp [hd, hdn, hn.ne']
no goals
R : Type u_1
inst✝ : Ring R
d n : ℕ
hdn : d ∣ n
hd : d ≠ 1
this : cyclotomic d ℤ ∣ ∑ i in range n, X ^ i
⊢ cyclotomic d R ∣ ∑ i in range n, X ^ i
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
  map_dvd (Int.castRingHom R) this
no goals
case inl
R : Type u_1
inst✝ : Ring R
d : ℕ
hd : d ≠ 1
hdn : d ∣ 0
⊢ cyclotomic d ℤ ∣ ∑ i in range 0, X ^ i
simp