:: deftheorem Def6 defines deg FIELD_4:def 7 :
for F being Field
for E being FieldExtension of F holds
( ( VecSp (E,F) is finite-dimensional implies deg (E,F) = dim (VecSp (E,F)) ) & ( not VecSp (E,F) is finite-dimensional implies deg (E,F) = - 1 ) );