:: deftheorem defines Gauss_INT_Field GAUSSINT:def 9 :
Gauss_INT_Field = the_Field_of_Quotients Gauss_INT_Ring;