equal
deleted
inserted
replaced
2188 hence "a=0" using assms(1) by auto |
2188 hence "a=0" using assms(1) by auto |
2189 thus ?thesis using `p=[:a:]` by simp |
2189 thus ?thesis using `p=[:a:]` by simp |
2190 qed |
2190 qed |
2191 |
2191 |
2192 |
2192 |
2193 section{*lead coefficient*} |
2193 subsection {* Leading coefficient *} |
2194 |
2194 |
2195 definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where |
2195 definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where |
2196 "lead_coeff p= coeff p (degree p)" |
2196 "lead_coeff p= coeff p (degree p)" |
2197 |
2197 |
2198 lemma lead_coeff_pCons[simp]: |
2198 lemma lead_coeff_pCons[simp]: |