:: deftheorem defines KrRoot FIELD_11:def 12 :
for F being Field
for m being Ordinal
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal holds KrRoot (I,m) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,<%(0. F),(1. F)%>)));