no goals
R✝ : Type ?u.32552
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ cyclotomic' 0 R = 1
simp only [cyclotomic', Finset.prod_empty, primitiveRoots_zero]