:: deftheorem defines deg_of_integral_element ALGNUM_1:def 10 :
for K, L being Field
for z being Element of L st K is Subring of L & z is_integral_over K holds
deg_of_integral_element (z,K) = deg (minimal_polynom (z,K));