formal lcm definition for polynomials

--- a/src/HOL/Library/Polynomial.thy	Thu Oct 02 11:33:06 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy	Thu Oct 02 11:33:08 2014 +0200
@@ -1724,6 +1724,10 @@
 
 declare gcd_poly.simps [simp del]
 
+definition lcm_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
+where
+  "lcm_poly a b = a * b div smult (coeff a (degree a) * coeff b (degree b)) (gcd a b)"
+
 instance ..
 
 end