:: deftheorem Def5 defines cyclotomic_poly UNIROOTS:def 5 :
for d being non zero Nat
for b₂ being Polynomial of F_Complex holds
( b₂ = cyclotomic_poly d iff ex s being non empty finite Subset of F_Complex st
( s = { y where y is Element of (MultGroup F_Complex) : ord y = d } & b₂ = poly_with_roots ((s,1) -bag) ) );