R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∑ i in range p, X ^ i
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p R = ∑ i in range p, X ^ i
suffices cyclotomic p ℤ = ∑ i in range p, X ^ i by
  simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
    congr_arg (map (Int.castRingHom R)) this
no goals
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
⊢ cyclotomic p ℤ = ∑ i in range p, X ^ i
rw [← prod_cyclotomic_eq_geom_sum hp.out.pos, hp.out.divisors,
  erase_insert (mem_singleton.not.2 hp.out.ne_one.symm), prod_singleton]
no goals
R : Type u_1
inst✝ : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
this : cyclotomic p ℤ = ∑ i in range p, X ^ i
⊢ cyclotomic p R = ∑ i in range p, X ^ i
simpa only [map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow, Polynomial.map_X] using
  congr_arg (map (Int.castRingHom R)) this