src/HOL/Computational_Algebra/Polynomial_Factorial.thy
changeset 66808 1907167b6038
parent 66806 a4e82b58d833
child 66817 0b12755ccbb2
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
     1.6    where "to_fract x = Fract x 1"
     1.7 -  \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
     1.8 +  \<comment> \<open>FIXME: more idiomatic name, abbreviation\<close>
     1.9  
    1.10  lemma to_fract_0 [simp]: "to_fract 0 = 0"
    1.11    by (simp add: to_fract_def eq_fract Zero_fract_def)
    1.12 @@ -438,8 +438,8 @@
    1.13      by (simp add: irreducible_dict)
    1.14    show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
    1.15      by (simp add: prime_elem_dict)
    1.16 -  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1 modulo
    1.17 -    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)
    1.18 +  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1
    1.19 +    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p) modulo
    1.20      (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
    1.21    proof (standard, fold dvd_dict)
    1.22      fix p :: "'a poly"