no goals
R✝ : Type ?u.33472
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ cyclotomic' 1 R = X - 1
simp only [cyclotomic', Finset.prod_singleton, RingHom.map_one,
  IsPrimitiveRoot.primitiveRoots_one]