R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ cyclotomic 1 R = X - 1
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 1 R = X - 1
have hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ := by
  simp only [cyclotomic'_one, PNat.one_coe, map_X, Polynomial.map_one, Polynomial.map_sub]
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = cyclotomic 1 R
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ cyclotomic 1 R = X - 1
symm
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (X - 1)
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = cyclotomic 1 R
rw [← map_cyclotomic_int, ← int_cyclotomic_unique hspec]
no goals
R : Type u_1
inst✝ : Ring R
hspec : map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
⊢ X - 1 = map (Int.castRingHom R) (X - 1)
simp only [map_X, Polynomial.map_one, Polynomial.map_sub]
no goals
R : Type u_1
inst✝ : Ring R
⊢ map (Int.castRingHom ℂ) (X - 1) = cyclotomic' 1 ℂ
simp only [cyclotomic'_one, PNat.one_coe, map_X, Polynomial.map_one, Polynomial.map_sub]