src/HOL/Library/Polynomial_Factorial.thy
changeset 64848 c50db2128048
parent 64795 8e7db8df16a0
child 64850 fc9265882329
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 15:54:48 2017 +0000
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 18:53:06 2017 +0100
     1.3 @@ -520,8 +520,8 @@
     1.4         (simp_all add: unit_factor_field_poly_def normalize_field_poly_def)
     1.5  next
     1.6    fix p :: "'a poly" assume "is_unit p"
     1.7 -  thus "normalize_field_poly p = 1"
     1.8 -    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
     1.9 +  then show "unit_factor_field_poly p = p"
    1.10 +    by (elim is_unit_polyE) (auto simp: unit_factor_field_poly_def monom_0 one_poly_def field_simps)
    1.11  next
    1.12    fix p :: "'a poly" assume "p \<noteq> 0"
    1.13    thus "is_unit (unit_factor_field_poly p)"
    1.14 @@ -566,7 +566,7 @@
    1.15  proof -
    1.16    have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
    1.17    have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
    1.18 -             normalize_field_poly unit_factor_field_poly" ..
    1.19 +             unit_factor_field_poly normalize_field_poly" ..
    1.20    from field_poly.in_prime_factors_imp_prime [of p x] assms
    1.21      show ?thesis unfolding prime_elem_def dvd_field_poly
    1.22        comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast