equal
deleted
inserted
replaced
221 |
221 |
222 |
222 |
223 subsection \<open>Mapping polynomials\<close> |
223 subsection \<open>Mapping polynomials\<close> |
224 |
224 |
225 definition map_poly |
225 definition map_poly |
226 :: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where |
226 :: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where |
227 "map_poly f p = Poly (map f (coeffs p))" |
227 "map_poly f p = Poly (map f (coeffs p))" |
228 |
228 |
229 lemma map_poly_0 [simp]: "map_poly f 0 = 0" |
229 lemma map_poly_0 [simp]: "map_poly f 0 = 0" |
230 by (simp add: map_poly_def) |
230 by (simp add: map_poly_def) |
231 |
231 |