equal
deleted
inserted
replaced
137 |
137 |
138 lemma lemma_order_pderiv1: |
138 lemma lemma_order_pderiv1: |
139 "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q + |
139 "pderiv ([:- a, 1:] ^ Suc n * q) = [:- a, 1:] ^ Suc n * pderiv q + |
140 smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)" |
140 smult (of_nat (Suc n)) (q * [:- a, 1:] ^ n)" |
141 apply (simp only: pderiv_mult pderiv_power_Suc) |
141 apply (simp only: pderiv_mult pderiv_power_Suc) |
142 apply (simp del: power_poly_Suc of_nat_Suc add: pderiv_pCons) |
142 apply (simp del: power_Suc of_nat_Suc add: pderiv_pCons) |
143 done |
143 done |
144 |
144 |
145 lemma dvd_add_cancel1: |
145 lemma dvd_add_cancel1: |
146 fixes a b c :: "'a::comm_ring_1" |
146 fixes a b c :: "'a::comm_ring_1" |
147 shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c" |
147 shows "a dvd b + c \<Longrightarrow> a dvd b \<Longrightarrow> a dvd c" |