# HG changeset patch
# User haftmann
# Date 1412242388 -7200
# Node ID 0bf0cf1d3547c5662b57646de0e004f310005521
# Parent  dc4d76dfa8f0b6b5d8a8c3757136d0fd45c916d3
formal lcm definition for polynomials

diff -r dc4d76dfa8f0 -r 0bf0cf1d3547 src/HOL/Library/Polynomial.thy
--- 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