# 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 \ 0 \ q \ 0 \ 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)