instance for polynomial rings with characteristic zero
authorhaftmann
Tue Apr 25 08:38:23 2017 +0200 (2017-04-25)
changeset 6557732d4117ad6e8
parent 65576 8376f83f9094
child 65578 e4997c181cce
instance for polynomial rings with characteristic zero
src/HOL/Computational_Algebra/Polynomial.thy
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Apr 24 23:10:01 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Tue Apr 25 08:38:23 2017 +0200
     1.3 @@ -1363,6 +1363,9 @@
     1.4  
     1.5  instance poly :: (idom) idom ..
     1.6  
     1.7 +instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0
     1.8 +  by standard (auto simp add: of_nat_poly intro: injI)
     1.9 +
    1.10  lemma degree_mult_eq: "p \<noteq> 0 \<Longrightarrow> q \<noteq> 0 \<Longrightarrow> degree (p * q) = degree p + degree q"
    1.11    for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
    1.12    by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)