# HG changeset patch
# User haftmann
# Date 1493102303 -7200
# Node ID 32d4117ad6e8070a813a393bb40da97732af4f60
# Parent  8376f83f909458ddba232454b62258b5f7ed5a06
instance for polynomial rings with characteristic zero

diff -r 8376f83f9094 -r 32d4117ad6e8 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Apr 24 23:10:01 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Tue Apr 25 08:38:23 2017 +0200
@@ -1363,6 +1363,9 @@
 
 instance poly :: (idom) idom ..
 
+instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0
+  by standard (auto simp add: of_nat_poly intro: injI)
+
 lemma degree_mult_eq: "p \<noteq> 0 \<Longrightarrow> q \<noteq> 0 \<Longrightarrow> degree (p * q) = degree p + degree q"
   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)