R✝ : Type ?u.78925
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ roots (∏ μ in primitiveRoots n R, (X - ↑C μ)) = (primitiveRoots n R).val
R✝ : Type ?u.78925
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ roots (cyclotomic' n R) = (primitiveRoots n R).val
rw [cyclotomic']
no goals
R✝ : Type ?u.78925
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ roots (∏ μ in primitiveRoots n R, (X - ↑C μ)) = (primitiveRoots n R).val
exact roots_prod_X_sub_C (primitiveRoots n R)