:: deftheorem defines KrRoot FIELD_1:def 6 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>);