src/HOL/Library/Polynomial.thy
changeset 62067 0fd850943901
parent 62065 1546a042e87b
child 62072 bf3d9f113474
equal deleted inserted replaced
62066:4db2d39aa76c 62067:0fd850943901
  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]: