for n being non zero Element of NAT
for f being FinSequence of the carrier of (Polynom-Ring F_Complex) st len f = n & ( for i being non zero Element of NAT st i in dom f holds
( ( not i divides n implies f . i = <%(1_ F_Complex)%> ) & ( i divides n implies f . i = cyclotomic_poly i ) ) ) holds
unital_poly (F_Complex,n) = Product f