# HG changeset patch
# User haftmann
# Date 1666938865 0
# Node ID 6bc3bb9d0e3eb2fc5f946cee0b7f9fee954948d0
# Parent  5ca3391244a3072550c32d83bc74848d9357ae5b
modulus for polynomials is invariant wrt. units

diff -r 5ca3391244a3 -r 6bc3bb9d0e3e src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Oct 28 13:18:27 2022 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Oct 28 06:34:25 2022 +0000
@@ -4064,6 +4064,25 @@
     by simp_all
 qed
 
+lemma mod_mult_unit_eq:
+  \<open>x mod (z * y) = x mod y\<close>
+  if \<open>is_unit z\<close>
+  for x y z :: \<open>'a::field poly\<close>
+proof (cases \<open>y = 0\<close>)
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  moreover have \<open>z \<noteq> 0\<close>
+    using that by auto
+  moreover define a where \<open>a = lead_coeff z\<close>
+  ultimately have \<open>z = [:a:]\<close> \<open>a \<noteq> 0\<close>
+    using that monom_0 [of a] by (simp_all add: is_unit_monom_trivial)
+  then show ?thesis
+    by (simp add: mod_smult_right)
+qed
+
 lemma poly_div_minus_right [simp]: "x div (- y) = - (x div y)"
   for x y :: "'a::field poly"
   using div_smult_right [of _ "- 1::'a"] by (simp add: nonzero_inverse_minus_eq)