n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
integer : ∏ i in Nat.divisors n, cyclotomic i ℤ = X ^ n - 1
⊢ ∏ i in Nat.divisors n, cyclotomic i R = X ^ n - 1
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Nat.divisors n, cyclotomic i R = X ^ n - 1
have integer : (∏ i in Nat.divisors n, cyclotomic i ℤ) = X ^ n - 1 := by
  apply map_injective (Int.castRingHom ℂ) Int.cast_injective
  simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X,
    Polynomial.map_one, Polynomial.map_sub]
  exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')
no goals
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
integer : ∏ i in Nat.divisors n, cyclotomic i ℤ = X ^ n - 1
⊢ ∏ i in Nat.divisors n, cyclotomic i R = X ^ n - 1
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sub, Polynomial.map_one,
  Polynomial.map_pow, Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) integer
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ map (Int.castRingHom ℂ) (∏ i in Nat.divisors n, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (X ^ n - 1)
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i in Nat.divisors n, cyclotomic i ℤ = X ^ n - 1
apply map_injective (Int.castRingHom ℂ) Int.cast_injective
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ x in Nat.divisors n, cyclotomic' x ℂ = X ^ n - 1
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ map (Int.castRingHom ℂ) (∏ i in Nat.divisors n, cyclotomic i ℤ) = map (Int.castRingHom ℂ) (X ^ n - 1)
simp only [Polynomial.map_prod, int_cyclotomic_spec, Polynomial.map_pow, map_X,
  Polynomial.map_one, Polynomial.map_sub]
no goals
case a
n : ℕ
hpos : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ x in Nat.divisors n, cyclotomic' x ℂ = X ^ n - 1
exact prod_cyclotomic'_eq_X_pow_sub_one hpos (Complex.isPrimitiveRoot_exp n hpos.ne')