src/HOL/Groebner_Basis.thy

 declare mod_div_trivial[algebra]
 declare mod_mod_trivial[algebra]
 declare mod_mult_self2_is_0[algebra]
 declare mod_mult_self1_is_0[algebra]
 declare zmod_eq_0_iff[algebra]
-declare zdvd_0_left[algebra]
+declare dvd_0_left_iff[algebra]
 declare zdvd1_eq[algebra]
 declare zmod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
 subsection{* Groebner Bases for fields *}