:: deftheorem defspl defines SplittingField FIELD_8:def 1 :
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for b₃ being FieldExtension of F holds
( b₃ is SplittingField of p iff ( p splits_in b₃ & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b₃ holds
E == b₃ ) ) );