src/HOL/Library/Polynomial_Factorial.thy
changeset 64242 93c6f0da5c70
parent 64240 eabf80376aab
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:04 2016 +0200
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Sun Oct 16 09:31:05 2016 +0200
     1.3 @@ -1038,7 +1038,7 @@
     1.4    thus "is_unit (unit_factor_field_poly p)"
     1.5      by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
     1.6  qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
     1.7 -       euclidean_size_field_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
     1.8 +       euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
     1.9  
    1.10  lemma field_poly_irreducible_imp_prime:
    1.11    assumes "irreducible (p :: 'a :: field poly)"
    1.12 @@ -1356,7 +1356,7 @@
    1.13    "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
    1.14  
    1.15  instance 
    1.16 -  by standard (auto simp: euclidean_size_poly_def Rings.mod_div_equality intro!: degree_mod_less' degree_mult_right_le)
    1.17 +  by standard (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
    1.18  end
    1.19  
    1.20