n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ = ∑ i in range n, X ^ i
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i R = ∑ i in range n, X ^ i
suffices (∏ i in n.divisors.erase 1, cyclotomic i ℤ) = ∑ i in Finset.range n, X ^ i by
  simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
    Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this
no goals
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ = ∑ i in range n, X ^ i
rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
  cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
no goals
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
this : ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i ℤ = ∑ i in range n, X ^ i
⊢ ∏ i in Finset.erase (Nat.divisors n) 1, cyclotomic i R = ∑ i in range n, X ^ i
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
  Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this