src/HOL/Library/Polynomial_Factorial.thy
changeset 63954 fb03766658f4
parent 63950 cdc1e59aa513
child 64164 38c407446400
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Wed Sep 28 17:02:06 2016 +0100
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Thu Sep 29 11:24:36 2016 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4  subsection \<open>Mapping polynomials\<close>
     1.5  
     1.6  definition map_poly 
     1.7 -     :: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
     1.8 +     :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
     1.9    "map_poly f p = Poly (map f (coeffs p))"
    1.10  
    1.11  lemma map_poly_0 [simp]: "map_poly f 0 = 0"