# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1556621865 -3600
# Node ID 8371a25ca1779cceda355e38ce1c88594efa9e08
# Parent  58191e01f0b13afc56347175854118a0af4ce8f7
Algebraic closure: moving more theorems into their rightful places

diff -r 58191e01f0b1 -r 8371a25ca177 NEWS
--- a/NEWS	Mon Apr 29 17:11:26 2019 +0100
+++ b/NEWS	Tue Apr 30 11:57:45 2019 +0100
@@ -266,7 +266,7 @@
 at the level of abstract topological spaces.
 
 * Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
-proofs towards algebraic closure by de Vilhena and Baillon.
+ algebraic closure of a field by de Vilhena and Baillon.
 
 * Session HOL-Homology has been added. It is a port of HOL Light's
 homology library, with new proofs of "invariance of domain" and related
diff -r 58191e01f0b1 -r 8371a25ca177 src/HOL/Algebra/Algebraic_Closure.thy
--- a/src/HOL/Algebra/Algebraic_Closure.thy	Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Algebraic_Closure.thy	Tue Apr 30 11:57:45 2019 +0100
@@ -61,7 +61,7 @@
 lemma (in field) law_restrict_is_field: "field (law_restrict R)"
 proof -
   have "comm_monoid_axioms (law_restrict R)"
-    using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto
+    using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto 
   then interpret L: cring "law_restrict R"
     using cring.intro law_restrict_is_ring comm_monoid.intro ring.is_monoid by auto
   have "Units R = Units (law_restrict R)"
@@ -69,7 +69,7 @@
   thus ?thesis
     using L.cring_fieldI unfolding field_Units law_restrict_carrier law_restrict_zero by simp
 qed
-
+    
 lemma law_restrict_iso_imp_eq:
   assumes "id \<in> ring_iso (law_restrict A) (law_restrict B)" and "ring A" and "ring B"
   shows "law_restrict A = law_restrict B"
@@ -108,33 +108,33 @@
 
 subsection \<open>Partial Order\<close>
 
-lemma iso_incl_backwards:
+lemma iso_incl_backwards: 
   assumes "A \<lesssim> B" shows "id \<in> ring_hom A B"
   using assms by cases
 
-lemma iso_incl_antisym_aux:
+lemma iso_incl_antisym_aux: 
   assumes "A \<lesssim> B" and "B \<lesssim> A" shows "id \<in> ring_iso A B"
-proof -
-  have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A"
+proof - 
+  have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A" 
     using assms(1-2)[THEN iso_incl_backwards] by auto
-  thus ?thesis
+  thus ?thesis 
     using hom[THEN ring_hom_memE(1)] by (auto simp add: ring_iso_def bij_betw_def inj_on_def)
 qed
 
-lemma iso_incl_refl: "A \<lesssim> A"
+lemma iso_incl_refl: "A \<lesssim> A" 
   by (rule iso_inclI[OF ring_hom_memI], auto)
 
-lemma iso_incl_trans:
+lemma iso_incl_trans: 
   assumes "A \<lesssim> B" and "B \<lesssim> C" shows "A \<lesssim> C"
   using ring_hom_trans[OF assms[THEN iso_incl_backwards]] by auto
 
 lemma (in ring) iso_incl_antisym:
   assumes "A \<in> \<S>" "B \<in> \<S>" and "A \<lesssim> B" "B \<lesssim> A" shows "A = B"
-proof -
-  obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
+proof - 
+  obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring" 
     where A: "A = law_restrict A'" "ring A'" and B: "B = law_restrict B'" "ring B'"
     using assms(1-2) field.is_ring by (auto simp add: extensions_def)
-  thus ?thesis
+  thus ?thesis 
     using law_restrict_iso_imp_eq iso_incl_antisym_aux[OF assms(3-4)] by simp
 qed
 
@@ -190,7 +190,7 @@
 subsection \<open>Chains\<close>
 
 definition union_ring :: "(('a, 'c) ring_scheme) set \<Rightarrow> 'a ring"
-  where "union_ring C =
+  where "union_ring C = 
            \<lparr> carrier = (\<Union>(carrier ` C)),
          monoid.mult = (\<lambda>a b. (monoid.mult (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b)),
                  one = one (SOME R. R \<in> C),
@@ -277,7 +277,7 @@
     using field_chain by simp
 
   show "a \<otimes>\<^bsub>union_ring C\<^esub> b \<in> carrier (union_ring C)"
-    using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto
+    using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto 
   show "(a \<otimes>\<^bsub>union_ring C\<^esub> b) \<otimes>\<^bsub>union_ring C\<^esub> c = a \<otimes>\<^bsub>union_ring C\<^esub> (b \<otimes>\<^bsub>union_ring C\<^esub> c)"
    and "a \<otimes>\<^bsub>union_ring C\<^esub> b = b \<otimes>\<^bsub>union_ring C\<^esub> a"
    and "\<one>\<^bsub>union_ring C\<^esub> \<otimes>\<^bsub>union_ring C\<^esub> a = a"
@@ -286,7 +286,7 @@
 next
   show "\<one>\<^bsub>union_ring C\<^esub> \<in> carrier (union_ring C)"
     using ring.ring_simprules(6)[OF ring_chain] assms same_one_same_zero(1)
-    unfolding union_ring_carrier by auto
+    unfolding union_ring_carrier by auto    
 qed
 
 lemma union_ring_is_abelian_group:
@@ -304,7 +304,7 @@
   show "(a \<oplus>\<^bsub>union_ring C\<^esub> b) \<otimes>\<^bsub>union_ring C\<^esub> c = (a \<otimes>\<^bsub>union_ring C\<^esub> c) \<oplus>\<^bsub>union_ring C\<^esub> (b \<otimes>\<^bsub>union_ring C\<^esub> c)"
    and "(a \<oplus>\<^bsub>union_ring C\<^esub> b) \<oplus>\<^bsub>union_ring C\<^esub> c = a \<oplus>\<^bsub>union_ring C\<^esub> (b \<oplus>\<^bsub>union_ring C\<^esub> c)"
    and "a \<oplus>\<^bsub>union_ring C\<^esub> b = b \<oplus>\<^bsub>union_ring C\<^esub> a"
-   and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a"
+   and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a" 
     using same_one_same_zero[OF R(1)] same_laws[OF R(1)] R(2-4) l_distr a_assoc a_comm by auto
   have "\<exists>a' \<in> carrier R. a' \<oplus>\<^bsub>union_ring C\<^esub> a = \<zero>\<^bsub>union_ring C\<^esub>"
     using same_laws(2)[OF R(1)] R(2) same_one_same_zero[OF R(1)] by simp
@@ -330,7 +330,7 @@
       using field_chain by simp
 
     from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>\<close> have "a \<in> Units R"
-      unfolding same_one_same_zero[OF R(1)] field_Units by auto
+      unfolding same_one_same_zero[OF R(1)] field_Units by auto 
     hence "\<exists>a' \<in> carrier R. a' \<otimes>\<^bsub>union_ring C\<^esub> a = \<one>\<^bsub>union_ring C\<^esub> \<and> a \<otimes>\<^bsub>union_ring C\<^esub> a' = \<one>\<^bsub>union_ring C\<^esub>"
       using same_laws[OF R(1)] same_one_same_zero[OF R(1)] R(2) unfolding Units_def by auto
     with \<open>R \<in> C\<close> and \<open>a \<in> carrier (union_ring C)\<close> show "a \<in> Units (union_ring C)"
@@ -457,11 +457,11 @@
   hence "set (map h p) \<subseteq> carrier S"
     by (induct p) (auto)
   moreover have "h a = \<zero>\<^bsub>S\<^esub> \<Longrightarrow> a = \<zero>\<^bsub>R\<^esub>" if "a \<in> carrier R" for a
-    using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp
+    using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp 
   with \<open>set p \<subseteq> carrier R\<close> have "lead_coeff (map h p) \<noteq> \<zero>\<^bsub>S\<^esub>" if "p \<noteq> []"
     using lc[OF that] that by (cases p) (auto)
   ultimately show ?thesis
-    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+    unfolding sym[OF univ_poly_carrier] polynomial_def by auto 
 qed
 
 lemma (in ring_hom_ring) subfield_polynomial_hom:
@@ -482,1147 +482,6 @@
 qed
 
 
-(* MOVE ========== *)
-subsection \<open>Roots and Multiplicity\<close>
-
-definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
-  where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
-
-definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
-  where "alg_mult p x =
-           (if p = [] then 0 else
-             (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
-
-definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
-  where "roots p = Abs_multiset (alg_mult p)"
-
-definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
-  where "roots_on K p = roots p \<inter># mset_set K"
-
-definition (in ring) splitted :: "'a list \<Rightarrow> bool"
-  where "splitted p \<longleftrightarrow> size (roots p) = degree p"
-
-definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
-  where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
-
-lemma (in domain) polynomial_pow_not_zero:
-  assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
-  shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  from assms UP.integral show ?thesis
-    unfolding sym[OF univ_poly_zero[of R "carrier R"]]
-    by (induction n, auto)
-qed
-
-lemma (in domain) subring_polynomial_pow_not_zero:
-  assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
-  shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
-  using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
-  unfolding univ_poly_consistent[OF assms(1)] by simp
-
-lemma (in domain) polynomial_pow_degree:
-  assumes "p \<in> carrier (poly_ring R)"
-  shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  show ?thesis
-  proof (induction n)
-    case 0 thus ?case
-      using UP.nat_pow_0 unfolding univ_poly_one by auto
-  next
-    let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
-    case (Suc n) thus ?case
-    proof (cases "p = []")
-      case True thus ?thesis
-        using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
-    next
-      case False
-      hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
-        using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
-      thus ?thesis
-        using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
-        unfolding univ_poly_carrier univ_poly_zero
-        by (auto simp add: add.commute univ_poly_mult)
-    qed
-  qed
-qed
-
-lemma (in domain) polynomial_pow_division:
-  assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
-  shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
-
-  have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
-    using assms(1) by (simp add: UP.nat_pow_mult)
-  thus ?thesis
-    using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
-    unfolding pdivides_def by auto
-qed
-
-lemma (in domain) degree_zero_imp_not_is_root:
-  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
-proof (cases "p = []", simp add: is_root_def)
-  case False with \<open>degree p = 0\<close> have "length p = Suc 0"
-    using le_SucE by fastforce
-  then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
-    using assms unfolding sym[OF univ_poly_carrier] polynomial_def
-    by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
-  thus ?thesis
-    unfolding is_root_def by auto
-qed
-
-lemma (in domain) is_root_imp_pdivides:
-  assumes "p \<in> carrier (poly_ring R)"
-  shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
-proof -
-  let ?b = "[ \<one> , \<ominus> x ]"
-
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
-    unfolding is_root_def by auto
-  hence b: "?b \<in> carrier (poly_ring R)"
-    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-  then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
-    and long_divides: "p = (?b \<otimes>\<^bsub>poly_ring R\<^esub> q) \<oplus>\<^bsub>poly_ring R\<^esub> r" "r = [] \<or> degree r < degree ?b"
-    using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
-
-  show ?thesis
-  proof (cases "r = []")
-    case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
-      unfolding univ_poly_zero[of R "carrier R"] .
-    thus ?thesis
-      using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
-  next
-    case False then have "length r = Suc 0"
-      using long_divides(2) le_SucE by fastforce
-    then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
-      using r unfolding sym[OF univ_poly_carrier] polynomial_def
-      by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
-
-    have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
-      using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
-    also have " ... = eval r x"
-      using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
-    finally have "a = \<zero>"
-      using a unfolding \<open>r = [ a ]\<close> is_root by simp
-    with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
-  qed
-qed
-
-lemma (in domain) pdivides_imp_is_root:
-  assumes "p \<noteq> []" and "x \<in> carrier R"
-  shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
-proof -
-  assume "[ \<one>, \<ominus> x ] pdivides p"
-  then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
-    unfolding pdivides_def by auto
-  moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
-    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
-  ultimately have "eval p x = \<zero>"
-    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
-  with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
-    unfolding is_root_def by simp
-qed
-
-lemma (in domain) associated_polynomials_imp_same_is_root:
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
-  shows "is_root p x \<longleftrightarrow> is_root q x"
-proof (cases "p = []")
-  case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
-    unfolding associated_def True factor_def univ_poly_def by auto
-  thus ?thesis
-    using True unfolding is_root_def by simp
-next
-  case False
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  { fix p q
-    assume p: "p \<in> carrier (poly_ring R)" and q: "q \<in> carrier (poly_ring R)" and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
-    have "is_root p x \<Longrightarrow> is_root q x"
-    proof -
-      assume is_root: "is_root p x"
-      then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
-        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
-      moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
-        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
-      ultimately have "[ \<one>, \<ominus> x ] pdivides q"
-        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
-      with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
-        using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
-              pdivides_imp_is_root[of q x]
-        by fastforce
-    qed
-  }
-
-  then show ?thesis
-    using assms UP.associated_sym[OF assms(3)] by blast
-qed
-
-lemma (in ring) monic_degree_one_root_condition:
-  assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
-  using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
-
-lemma (in field) degree_one_root_condition:
-  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
-  shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
-    by simp
-  then obtain a b where p: "p = [ a, b ]"
-    by (metis length_0_conv length_Cons list.exhaust nat.inject)
-  hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
-    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-  hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
-    using subfield_m_inv[OF carrier_is_subfield, of a] by auto
-  hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
-    using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-
-  have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
-  proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
-    have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
-      using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
-    also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
-      using UP.m_comm[OF in_carrier, of "[ a ]"] a
-      by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
-    finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
-  next
-    from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
-      unfolding univ_poly_units[OF carrier_is_subfield] by simp
-  qed
-
-  moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
-    and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
-    using inv_a a b unfolding p const_term_def by auto
-
-  ultimately show ?thesis
-    using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
-          monic_degree_one_root_condition
-    by (metis add.inv_closed)
-qed
-
-lemma (in domain) is_root_imp_is_root_poly_mult:
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "q \<noteq> []"
-  shows "is_root p x \<Longrightarrow> is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  assume "is_root p x" then have x: "x \<in> carrier R" and eval: "eval p x = \<zero>" and not_zero: "p \<noteq> []"
-    unfolding is_root_def by simp+
-  hence "p \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
-    using assms UP.integral unfolding sym[OF univ_poly_zero[of R "carrier R"]] by blast
-  moreover have "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
-    using assms eval ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by auto
-  ultimately show ?thesis
-    using x unfolding is_root_def by simp
-qed
-
-lemma (in domain) is_root_poly_mult_imp_is_root:
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
-  shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
-  hence "p \<noteq> []" and "q \<noteq> []"
-    unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
-    using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
-  moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
-    using is_root unfolding is_root_def by simp+
-  hence "eval p x = \<zero> \<or> eval q x = \<zero>"
-    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto
-  ultimately show "(is_root p x) \<or> (is_root q x)"
-    using x unfolding is_root_def by auto
-qed
-
-(*
-lemma (in domain)
-  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
-  shows "pprime K p"
-proof (rule pprimeI[OF assms(1-2)])
-  from \<open>degree p = 1\<close> show "p \<noteq> []" and "p \<notin> Units (K [X])"
-    unfolding univ_poly_units[OF assms(1)] by auto
-next
-  fix q r
-  assume "q \<in> carrier (K[X])" and "r \<in> carrier (K[X])"
-    and pdiv: "p pdivides q \<otimes>\<^bsub>K [X]\<^esub> r"
-  hence "q \<in> carrier (poly_ring R)" and "r \<in> carrier (poly_ring R)"
-    using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
-  moreover obtain b where b: "b \<in>"
-qed
-*)
-
-lemma (in domain) finite_number_of_roots:
-  assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
-  using assms
-proof (induction "degree p" arbitrary: p)
-  case 0 thus ?case
-    by (simp add: degree_zero_imp_not_is_root)
-next
-  case (Suc n) show ?case
-  proof (cases "{ x. is_root p x } = {}")
-    case True thus ?thesis
-      by (simp add: True)
-  next
-    interpret UP: domain "poly_ring R"
-      using univ_poly_is_domain[OF carrier_is_subring] .
-
-    case False
-    then obtain a where is_root: "is_root p a"
-      by blast
-    hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
-      unfolding is_root_def by auto
-    hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
-      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-
-    obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
-      using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
-    with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
-      using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
-      by metis
-    hence "degree q = n"
-      using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
-            in_carrier q p_not_zero p Suc(2)
-      unfolding univ_poly_carrier
-      by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
-                list.size(3-4) plus_1_eq_Suc univ_poly_mult)
-    hence "finite { x. is_root q x }"
-      using Suc(1)[OF _ q] by simp
-
-    moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
-      using is_root_poly_mult_imp_is_root[OF in_carrier q]
-            monic_degree_one_root_condition[OF a]
-      unfolding p by auto
-
-    ultimately show ?thesis
-      using finite_subset by auto
-  qed
-qed
-
-lemma (in domain) alg_multE:
-  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
-  shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
-    and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
-
-  define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
-  have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
-    using UP.nat_pow_0 by simp
-  hence "0 \<in> S"
-    using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
-  hence "S \<noteq> {}"
-    by auto
-
-  moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
-  proof -
-    have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
-      using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-    hence "?ppow n \<in> carrier (poly_ring R)"
-      using assms unfolding univ_poly_zero by auto
-    with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
-      using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
-    with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
-      using polynomial_pow_degree by simp
-  qed
-  hence "finite S"
-    using finite_nat_set_iff_bounded_le by blast
-
-  ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
-    using Max_ge[of S] Max_in[of S] by auto
-  with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
-    using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
-    unfolding S_def alg_mult_def by auto
-  thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
-   and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
-    using MaxS unfolding S_def by auto
-qed
-
-lemma (in domain) le_alg_mult_imp_pdivides:
-  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
-  shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  assume le_alg_mult: "n \<le> alg_mult p x"
-  have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
-    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-  hence ppow_pdivides:
-    "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
-     ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
-    using polynomial_pow_division[OF _ le_alg_mult] by simp
-
-  show ?thesis
-  proof (cases "p = []")
-    case True thus ?thesis
-      using in_carrier pdivides_zero[OF carrier_is_subring] by auto
-  next
-    case False thus ?thesis
-      using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
-      unfolding pdivides_def by meson
-  qed
-qed
-
-lemma (in domain) alg_mult_gt_zero_iff_is_root:
-  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-  show ?thesis
-  proof
-    assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
-      unfolding is_root_def by auto
-    have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
-      using x unfolding univ_poly_def by auto
-    thus "alg_mult p x > 0"
-      using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
-  next
-    assume gt_zero: "alg_mult p x > 0"
-    hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
-      unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
-    hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
-      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-    with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
-      using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
-    thus "is_root p x"
-      using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
-  qed
-qed
-
-lemma (in domain) alg_mult_in_multiset:
-  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p \<in> multiset"
-  using assms alg_mult_gt_zero_iff_is_root finite_number_of_roots unfolding multiset_def by auto
-
-lemma (in domain) alg_mult_eq_count_roots:
-  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
-  using alg_mult_in_multiset[OF assms] by (simp add: roots_def)
-
-lemma (in domain) roots_mem_iff_is_root:
-  assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
-  using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
-  unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
-
-lemma (in domain) degree_zero_imp_empty_roots:
-  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
-proof -
-  have "alg_mult p = (\<lambda>x. 0)"
-  proof (cases "p = []")
-    case True thus ?thesis
-      using assms unfolding alg_mult_def by auto
-  next
-    case False hence "length p = Suc 0"
-      using assms(2) by (simp add: le_Suc_eq)
-    then obtain a where "a \<in> carrier R" and "a \<noteq> \<zero>" and p: "p = [ a ]"
-      using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def
-      by (metis Suc_length_conv hd_in_set length_0_conv list.sel(1) subset_code(1))
-    show ?thesis
-    proof (rule ccontr)
-      assume "alg_mult p \<noteq> (\<lambda>x. 0)"
-      then obtain x where "alg_mult p x > 0"
-        by auto
-      with \<open>p \<noteq> []\<close> have "eval p x = \<zero>"
-        using alg_mult_gt_zero_iff_is_root[OF assms(1), of x] unfolding is_root_def by simp
-      with \<open>a \<in> carrier R\<close> have "a = \<zero>"
-        unfolding p by auto
-      with \<open>a \<noteq> \<zero>\<close> show False ..
-    qed
-  qed
-  thus ?thesis
-    by (simp add: roots_def zero_multiset.abs_eq)
-qed
-
-lemma (in domain) degree_zero_imp_splitted:
-  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
-  unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
-
-lemma (in domain) roots_inclI':
-  assumes "p \<in> carrier (poly_ring R)" and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> alg_mult p a \<le> count m a"
-  shows "roots p \<subseteq># m"
-proof (intro mset_subset_eqI)
-  fix a show "count (roots p) a \<le> count m a"
-    using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
-    by (cases "p = []", simp, cases "a \<in> carrier R", auto)
-qed
-
-lemma (in domain) roots_inclI:
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
-    and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
-  shows "roots p \<subseteq># roots q"
-  using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
-  unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
-
-lemma (in domain) pdivides_imp_roots_incl:
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
-  shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
-proof (rule roots_inclI[OF assms])
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  fix a assume "p pdivides q" and a: "a \<in> carrier R"
-  hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
-    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
-  with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
-    using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
-    by (auto simp add: pdivides_def)
-qed
-
-lemma (in domain) associated_polynomials_imp_same_roots:
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
-  shows "roots p = roots q"
-  using assms pdivides_imp_roots_incl zero_pdivides
-  unfolding pdivides_def associated_def
-  by (metis subset_mset.eq_iff)
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in comm_monoid_cancel) prime_pow_divides_iff:
-  assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
-  shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
-proof
-  assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
-    using divides_prod_l[of "p [^] n" b a] assms by simp
-next
-  assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
-  proof (induction n)
-    case 0 with \<open>b \<in> carrier G\<close> show ?case
-      by (simp add: unit_divides)
-  next
-    case (Suc n)
-    hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
-      using assms(1) divides_prod_r by auto
-    with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
-      where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
-        and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
-      using assms by blast
-    hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
-      using assms by (simp add: m_assoc m_lcomm)
-    hence "a \<otimes> c = p \<otimes> d"
-      using c d assms(1) assms(2) l_cancel by blast
-    with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
-      by (metis assms(2) c d dividesI' prime_divides)
-    with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
-      using assms(1) c by simp
-  qed
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) pirreducible_pow_pdivides_iff:
-  assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
-    and "pirreducible K p" and "\<not> (p pdivides q)"
-  shows "(p [^]\<^bsub>K[X]\<^esub> (n :: nat)) pdivides (q \<otimes>\<^bsub>K[X]\<^esub> r) \<longleftrightarrow> (p [^]\<^bsub>K[X]\<^esub> n) pdivides r"
-proof -
-  interpret UP: principal_domain "K[X]"
-    using univ_poly_is_principal[OF assms(1)] .
-  show ?thesis
-  proof (cases "r = []")
-    case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
-      unfolding  sym[OF univ_poly_zero[of R K]] by auto
-    thus ?thesis
-      using pdivides_zero[OF subfieldE(1),of K] assms by auto
-  next
-    case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
-      using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
-            UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
-    from \<open>p \<noteq> []\<close>
-    have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
-      using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
-    have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
-      using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
-    have prime: "prime (mult_of (K[X])) p"
-      using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
-      unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
-    have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
-      if "a \<in> carrier (K[X])" "a \<noteq> \<zero>\<^bsub>K[X]\<^esub>" "b \<in> carrier (K[X])" "b \<noteq> \<zero>\<^bsub>K[X]\<^esub>" for a b
-      using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
-      unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
-    thus ?thesis
-      using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
-      unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
-      by (metis DiffI UP.m_closed singletonD)
-  qed
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) univ_poly_units':
-  assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
-  unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
-  by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) subring_degree_one_imp_pirreducible:
-  assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
-  shows "pirreducible K [ a, b ]"
-proof (rule pirreducibleI[OF assms(1)])
-  have "a \<in> K" and "a \<noteq> \<zero>"
-    using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
-  thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
-    using univ_poly_units_incl[OF assms(1)] assms(2-3)
-    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-next
-  interpret UP: domain "K[X]"
-    using univ_poly_is_domain[OF assms(1)] .
-
-  { fix q r
-    assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
-    hence not_zero: "q \<noteq> []" "r \<noteq> []"
-      by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
-    have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
-      using not_zero poly_mult_degree_eq[OF assms(1)] q r
-      by (simp add: univ_poly_carrier univ_poly_mult)
-    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
-      using not_zero by auto
-  } note aux_lemma1 = this
-
-  { fix q r
-    assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
-      and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
-    hence "length q = Suc (Suc 0)" and "length r = Suc 0"
-      by (linarith, metis add.right_neutral add_eq_if length_0_conv)
-    from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
-      by (metis length_0_conv length_Cons list.exhaust nat.inject)
-    from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
-      by (metis length_0_conv length_Suc_conv)
-    from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
-    have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
-      using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
-      using poly_mult_lead_coeff[OF assms(1), of q r]
-      unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
-    obtain inv_a where a: "a \<in> K" and inv_a: "inv_a \<in> K" "a \<otimes> inv_a = \<one>" "inv_a \<otimes> a = \<one>"
-      using assms(2) unfolding Units_def by auto
-    hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
-      using subringE(1)[OF assms(1)] integral_iff by auto
-    with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
-      using subringE(1,6)[OF assms(1)] inv_a integral
-      unfolding sym[OF univ_poly_carrier] polynomial_def
-      by (auto, meson subsetD)
-    moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
-      using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
-      unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
-    ultimately have "r \<in> Units (K[X])"
-      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
-  } note aux_lemma2 = this
-
-  fix q r
-  assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and qr: "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
-  thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
-    using aux_lemma1[OF q r qr] aux_lemma2[of q r] aux_lemma2[of r q] UP.m_comm add_is_1 by auto
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) degree_one_imp_pirreducible:
-  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
-  shows "pirreducible K p"
-proof -
-  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
-    by simp
-  then obtain a b where p: "p = [ a, b ]"
-    by (metis length_0_conv length_Suc_conv)
-  with \<open>p \<in> carrier (K[X])\<close> show ?thesis
-    using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
-          subfield.subfield_Units[OF assms(1)]
-    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in ring) degree_oneE[elim]:
-  assumes "p \<in> carrier (K[X])" and "degree p = 1"
-    and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
-  shows P
-proof -
-  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
-    by simp
-  then obtain a b where "p = [ a, b ]"
-    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
-  with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
-    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-  with \<open>p = [ a, b ]\<close> show ?thesis
-    using assms(3) by simp
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) subring_degree_one_associatedI:
-  assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
-  shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
-proof -
-  from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
-    using subringE(1)[OF assms(1)] assms(2-3) by auto
-  hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
-    using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
-    unfolding univ_poly_mult by fastforce
-  moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
-    using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
-    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-  moreover have "[ a ] \<in> Units (K[X])"
-  proof -
-    from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
-      using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-    moreover have "a' \<otimes> a = \<one>"
-      using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp
-    hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
-      using assms unfolding univ_poly_mult by auto
-    ultimately show ?thesis
-      unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
-  qed
-  ultimately show ?thesis
-    using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
-qed
-
-(* MOVE to Polynomial_Divisibility.thy *)
-lemma (in domain) degree_one_associatedI:
-  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
-  shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
-proof -
-  from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
-  obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
-    by auto
-  thus ?thesis
-    using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
-          subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
-    unfolding const_term_def
-    by auto
-qed
-
-lemma (in domain) monic_degree_one_roots:
-  assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
-proof -
-  let ?p = "[ \<one> , \<ominus> a ]"
-
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
-    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
-  show ?thesis
-  proof (rule subset_mset.antisym)
-    show "{# a #} \<subseteq># roots ?p"
-      using roots_mem_iff_is_root[OF in_carrier]
-            monic_degree_one_root_condition[OF assms]
-      by simp
-  next
-    show "roots ?p \<subseteq># {# a #}"
-    proof (rule mset_subset_eqI, auto)
-      fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
-        using alg_mult_gt_zero_iff_is_root[OF in_carrier]
-              monic_degree_one_root_condition[OF assms]
-        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
-        by fastforce
-    next
-      have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
-        using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
-      hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
-        using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
-      thus "count (roots ?p) a \<le> Suc 0"
-        using polynomial_pow_degree[OF in_carrier]
-        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
-        by auto
-    qed
-  qed
-qed
-
-lemma (in domain) degree_one_roots:
-  assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
-  shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
-proof -
-  have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
-    using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-  thus ?thesis
-    using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
-          monic_degree_one_roots associated_polynomials_imp_same_roots
-    by (metis add.inv_closed local.minus_minus m_closed)
-qed
-
-lemma (in field) degree_one_imp_singleton_roots:
-  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
-  shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
-proof -
-  from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
-  obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
-    by auto
-  thus ?thesis
-    using degree_one_roots[of a "inv a" b]
-    by (auto simp add: const_term_def field_Units)
-qed
-
-lemma (in field) degree_one_imp_splitted:
-  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
-  using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
-
-lemma (in field) no_roots_imp_same_roots:
-  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
-  shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
-  proof (intro subset_mset.antisym)
-    have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
-      using UP.divides_prod_l assms unfolding pdivides_def by blast
-    show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
-      using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
-            degree_zero_imp_empty_roots[OF assms(3)]
-      by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
-  next
-    show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
-    proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
-      case True thus ?thesis
-        using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
-    next
-      case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
-        by (metis UP.r_null assms(1) univ_poly_zero)
-      show ?thesis
-      proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
-        fix a assume a: "a \<in> carrier R"
-        hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
-          using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
-        moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
-          using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-        hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
-          using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
-        moreover
-        have "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
-          using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
-        ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
-          using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
-      qed
-    qed
-  qed
-qed
-
-lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
-  assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
-  shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-
-  from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
-    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
-
-  show ?thesis
-  proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
-    show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
-      using in_carrier assms(2) by simp
-  next
-    fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
-    hence not_zero: "p \<noteq> []"
-      unfolding univ_poly_def by auto
-    from \<open>b \<in> carrier R\<close> have in_carrier':  "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
-      unfolding sym[OF univ_poly_carrier] polynomial_def by simp
-    show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
-    proof (cases "a = b")
-      case False
-      hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
-        using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
-      moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
-        using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
-      ultimately
-      have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
-        using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
-              pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
-        by auto
-      with \<open>a \<noteq> b\<close> show ?thesis
-        using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
-    next
-      case True
-      have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
-        using dividesI[OF assms(2)] unfolding pdivides_def by auto
-      with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
-      have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
-        using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
-      then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
-        using Suc_le_D by blast
-      hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
-             ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
-        using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
-              in_carrier assms UP.nat_pow_Suc2 by force
-      hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
-        using UP.mult_divides in_carrier assms(2)
-        unfolding univ_poly_zero pdivides_def factor_def
-        by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
-      with \<open>a = b\<close> show ?thesis
-        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
-              alg_multE(2)[OF assms(1) _ not_zero] m
-        by auto
-    qed
-  next
-    fix b
-    have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
-      using assms in_carrier univ_poly_zero[of R] UP.integral by auto
-
-    show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
-    proof (cases "a = b")
-      case True
-      have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
-            ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
-        using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
-        by (auto simp add: pdivides_def)
-      with \<open>a = b\<close> show ?thesis
-        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
-              alg_multE(2)[OF assms(1) _ not_zero]
-        by auto
-    next
-      case False
-      have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
-        using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
-      thus ?thesis
-        using False pdivides_imp_roots_incl assms in_carrier not_zero
-        by (simp add: subseteq_mset_def)
-    qed
-  qed
-qed
-
-lemma (in domain) not_empty_rootsE[elim]:
-  assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
-    and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
-               [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
-  shows P
-proof -
-  from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
-    by blast
-  with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
-    and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
-    using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
-    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
-  with \<open>a \<in># roots p\<close> show ?thesis
-    using assms(3)[of a] by auto
-qed
-
-lemma (in field) associated_polynomials_imp_same_roots:
-  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
-  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots p + roots q"
-proof -
-  interpret UP: domain "poly_ring R"
-    using univ_poly_is_domain[OF carrier_is_subring] .
-  from assms show ?thesis
-  proof (induction "degree p" arbitrary: p rule: less_induct)
-    case less show ?case
-    proof (cases "roots p = {#}")
-      case True thus ?thesis
-        using no_roots_imp_same_roots[of p q] less by simp
-    next
-      case False with \<open>p \<in> carrier (poly_ring R)\<close>
-      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
-          and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
-        by blast
-      show ?thesis
-      proof (cases "degree p = 1")
-        case True with \<open>p \<in> carrier (poly_ring R)\<close>
-        obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
-          by auto
-        with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
-          and lead: "lead_coeff p = b" and const: "const_term p = c"
-          using degree_one_imp_singleton_roots[of p] less(2) field_Units
-          unfolding const_term_def by auto
-        hence "(p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<sim>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
-          using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
-          by (auto simp add: a lead const)
-        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
-          using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
-        thus ?thesis
-          unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
-      next
-        case False
-        from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
-        obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
-          unfolding pdivides_def by auto
-        with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
-          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
-        with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
-          using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
-          unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
-        with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
-          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
-        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
-          using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
-                UP.m_assoc[OF in_carrier r less(4)] p by auto
-        also have " ... = add_mset a (roots r + roots q)"
-          using less(1)[OF _ r not_zero less(4-5)] deg by simp
-        also have " ... = (add_mset a (roots r)) + roots q"
-          by simp
-        also have " ... = roots p + roots q"
-          using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp
-        finally show ?thesis .
-      qed
-    qed
-  qed
-qed
-
-lemma (in field) size_roots_le_degree:
-  assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
-  using assms
-proof (induction "degree p" arbitrary: p rule: less_induct)
-  case less show ?case
-  proof (cases "roots p = {#}", simp)
-    interpret UP: domain "poly_ring R"
-      using univ_poly_is_domain[OF carrier_is_subring] .
-
-    case False with \<open>p \<in> carrier (poly_ring R)\<close>
-    obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
-      and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
-      by blast
-    then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
-      unfolding pdivides_def by auto
-    with \<open>a \<in># roots p\<close> have "p \<noteq> []"
-      using degree_zero_imp_empty_roots[OF less(2)] by auto
-    hence not_zero: "q \<noteq> []"
-      using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
-    hence "degree p = Suc (degree q)"
-      using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
-      unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
-    with \<open>q \<noteq> []\<close> show ?thesis
-      using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
-      by (metis Suc_le_mono lessI size_add_mset)
-  qed
-qed
-
-
-(* MOVE to Polynomial_Divisibility.thy ======== *)
-lemma (in ring) divides_pirreducible_condition:
-  assumes "pirreducible K q" and "p \<in> carrier (K[X])"
-  shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
-  using divides_irreducible_condition[of "K[X]" q p] assms
-  unfolding ring_irreducible_def by auto
-
-lemma (in domain) pirreducible_roots:
-  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
-  shows "roots p = {#}"
-proof (rule ccontr)
-  assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
-  obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
-    and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
-    by blast
-  hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
-    using divides_pirreducible_condition[OF assms(2) in_carrier]
-          univ_poly_units_incl[OF carrier_is_subring]
-    unfolding pdivides_def by auto
-  hence "degree p = 1"
-    using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
-  with \<open>degree p \<noteq> 1\<close> show False ..
-qed
-
-lemma (in field) pirreducible_imp_not_splitted:
-  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
-  shows "\<not> splitted p"
-  using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
-  by (simp add: splitted_def)
-
-lemma (in field)
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
-    and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
-  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
-  using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
-  unfolding ring_irreducible_def univ_poly_zero by auto
-
-lemma (in field) trivial_factors_imp_splitted:
-  assumes "p \<in> carrier (poly_ring R)"
-    and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
-  shows "splitted p"
-  using assms
-proof (induction "degree p" arbitrary: p rule: less_induct)
-  interpret UP: principal_domain "poly_ring R"
-    using univ_poly_is_principal[OF carrier_is_subfield] .
-  case less show ?case
-  proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
-    case False show ?thesis
-    proof (cases "roots p = {#}")
-      case True
-      from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
-        using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
-      then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
-        using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
-      with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
-        using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
-              pdivides_imp_roots_incl[OF _ less(2), of q]
-              pirreducible_degree[OF carrier_is_subfield, of q]
-        by force
-      from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
-        by simp
-      thus ?thesis ..
-    next
-      case False with \<open>p \<in> carrier (poly_ring R)\<close>
-      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
-        and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
-        by blast
-      then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
-        unfolding pdivides_def by blast
-      with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
-        by auto
-      with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
-        using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
-      with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> and \<open>p \<noteq> []\<close> have "degree p = Suc (degree q)"
-        using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
-        unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
-      moreover have "q pdivides p"
-        using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
-      hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
-        and "r pdivides q" for r
-        using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
-              pirreducible_degree[OF carrier_is_subfield that(1-2)]
-        by (auto simp add: pdivides_def)
-      ultimately have "splitted q"
-        using less(1)[OF _ q] by auto
-      with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
-        using poly_mult_degree_one_monic_imp_same_roots[OF a q]
-        unfolding sym[OF p] splitted_def
-        by simp
-    qed
-  qed
-qed
-
-lemma (in field) pdivides_imp_splitted:
-  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q"
-  shows "p pdivides q \<Longrightarrow> splitted p"
-proof (cases "p = []")
-  case True thus ?thesis
-    using degree_zero_imp_splitted[OF assms(1)] by simp
-next
-  interpret UP: principal_domain "poly_ring R"
-    using univ_poly_is_principal[OF carrier_is_subfield] .
-
-  case False
-  assume "p pdivides q"
-  then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
-    unfolding pdivides_def by auto
-  with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
-    using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
-  hence "degree p + degree b = size (roots p) + size (roots b)"
-    using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
-          poly_mult_degree_eq[OF carrier_is_subring,of p b]
-    unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
-    by auto
-  moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
-    using size_roots_le_degree assms(1) b by auto
-  ultimately show ?thesis
-    unfolding splitted_def by linarith
-qed
-
-lemma (in field) splitted_imp_trivial_factors:
-  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
-  shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
-  using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
-  by auto
-
 lemma (in field) exists_root:
   assumes "M \<in> extensions" and "\<And>L. \<lbrakk> L \<in> extensions; M \<lesssim> L \<rbrakk> \<Longrightarrow> law_restrict L = law_restrict M"
     and "P \<in> carrier (poly_ring R)"
@@ -1664,7 +523,7 @@
   qed
   then obtain i :: nat where "\<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
     by blast
-
+  
   then have hyps:
     \<comment> \<open>i\<close>   "field M"
     \<comment> \<open>ii\<close>  "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> carrier_coeff \<P>"
@@ -1760,7 +619,7 @@
   obtain M where "M \<in> extensions" and "\<forall>L \<in> extensions. M \<lesssim> L \<longrightarrow> law_restrict L = law_restrict M"
     using exists_maximal_extension iso_incl_hom by blast
   thus ?thesis
-    using exists_root[of M] by auto
+    using exists_root[of M] by auto 
 qed
 
 
@@ -1773,9 +632,9 @@
 locale algebraically_closed = field L for L (structure) +
   assumes roots_over_carrier: "P \<in> carrier (poly_ring L) \<Longrightarrow> splitted P"
 
-definition (in field) closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring" ("\<Omega>")
-  where "closure = (SOME L \<comment> \<open>such that\<close>.
-           \<comment> \<open>i\<close>  algebraic_closure L (indexed_const ` (carrier R)) \<and>
+definition (in field) alg_closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
+  where "alg_closure = (SOME L \<comment> \<open>such that\<close>.
+           \<comment> \<open>i\<close>  algebraic_closure L (indexed_const ` (carrier R)) \<and> 
            \<comment> \<open>ii\<close> indexed_const \<in> ring_hom R L)"
 
 lemma algebraic_hom:
@@ -1961,7 +820,7 @@
             with \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close>
             have "degree R = 1"
               using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M]
-                    Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force
+                    Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force  
             thus ?thesis
               by simp
           qed
@@ -1978,11 +837,26 @@
     using that by auto
 qed
 
-lemma (in field) closureE:
-  shows "algebraic_closure \<Omega> (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R \<Omega>"
-  using exists_closure unfolding closure_def
+lemma (in field) alg_closureE:
+  shows "algebraic_closure alg_closure (indexed_const ` (carrier R))"
+    and "indexed_const \<in> ring_hom R alg_closure"
+  using exists_closure unfolding alg_closure_def
   by (metis (mono_tags, lifting) someI2)+
 
+lemma (in field) algebraically_closedI':
+  assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> splitted p"
+  shows "algebraically_closed R"
+proof
+  fix p assume "p \<in> carrier (poly_ring R)" show "splitted p"
+  proof (cases "degree p \<le> 1")
+    case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
+      using degree_zero_imp_splitted degree_one_imp_splitted by fastforce
+  next
+    case False with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
+      using assms by fastforce
+  qed
+qed
+
 lemma (in field) algebraically_closedI:
   assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier R. eval p x = \<zero>"
   shows "algebraically_closed R"
@@ -2014,13 +888,13 @@
       moreover have "roots p = add_mset a (roots q)"
         using poly_mult_degree_one_monic_imp_same_roots[OF a(1) q not_zero] p by simp
       ultimately show ?thesis
-        unfolding splitted_def deg by simp
+        unfolding splitted_def deg by simp 
     qed
   qed
 qed
 
 sublocale algebraic_closure \<subseteq> algebraically_closed
-proof (rule algebraically_closedI)
+proof (rule algebraically_closedI')
   fix P assume in_carrier: "P \<in> carrier (poly_ring L)" and gt_one: "degree P > 1"
   then have gt_zero: "degree P > 0"
     by simp
@@ -2074,11 +948,11 @@
           univ_poly_subfield_of_consts[OF subfield_axioms] by auto
 
   moreover from \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "poly_of_const ` K \<subseteq> carrier (A[X])"
-    using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp
+    using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp 
 
   ultimately
   have "subalgebra (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X])) (Rupt A P)"
-    using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp
+    using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp 
 
   moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carrier (Rupt A P))"
   proof (intro Rupt.telescopic_base_dim(1)[where
@@ -2113,7 +987,7 @@
 
   ultimately
   have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X]))"
-    using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp
+    using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp 
 
   hence "\<not> inj_on (rupture_surj A P) (carrier (K[X]))"
     using Hom'.infinite_dimension_hom[OF _ rupture_one_not_zero[OF A P gt_zero] _
@@ -2129,14 +1003,11 @@
     unfolding cgenideal_def by blast
   with \<open>P \<in> carrier (A[X])\<close> have "P pdivides Q"
     using dividesI[of _ "A[X]"] UP_A.m_comm pdivides_iff_shell[OF A] by simp
-  hence "splitted P"
+  thus "splitted P"
     using pdivides_imp_splitted[OF in_carrier
           carrier_polynomial_shell[OF subfieldE(1)[OF subfield_axioms] Q(1)] Q(2)
-          roots_over_subfield[OF Q(1)]] Q by simp
-  with \<open>degree P > 1\<close> obtain a where "a \<in># roots P"
-    unfolding splitted_def by force
-  thus "\<exists>x\<in>carrier L. eval P x = \<zero>"
-    unfolding roots_mem_iff_is_root[OF in_carrier] is_root_def by blast
+          roots_over_subfield[OF Q(1)]] Q
+    by simp
 qed
 
 end
diff -r 58191e01f0b1 -r 8371a25ca177 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Tue Apr 30 11:57:45 2019 +0100
@@ -780,6 +780,36 @@
     using A(1) Units_one_closed b'(1) unit_factor by presburger
 qed
 
+lemma (in comm_monoid_cancel) prime_pow_divides_iff:
+  assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
+  shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
+proof
+  assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
+    using divides_prod_l[of "p [^] n" b a] assms by simp  
+next
+  assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
+  proof (induction n)
+    case 0 with \<open>b \<in> carrier G\<close> show ?case
+      by (simp add: unit_divides)
+  next
+    case (Suc n)
+    hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
+      using assms(1) divides_prod_r by auto
+    with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
+      where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
+        and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
+      using assms by blast
+    hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
+      using assms by (simp add: m_assoc m_lcomm)
+    hence "a \<otimes> c = p \<otimes> d"
+      using c d assms(1) assms(2) l_cancel by blast
+    with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
+      by (metis assms(2) c d dividesI' prime_divides)
+    with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
+      using assms(1) c by simp
+  qed
+qed
+
 
 subsection \<open>Factorization and Factorial Monoids\<close>
 
diff -r 58191e01f0b1 -r 8371a25ca177 src/HOL/Algebra/Finite_Extensions.thy
--- a/src/HOL/Algebra/Finite_Extensions.thy	Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Finite_Extensions.thy	Tue Apr 30 11:57:45 2019 +0100
@@ -293,8 +293,11 @@
         using assms(1) lin(2) unfolding polynomial_def by auto
       hence "eval (normalize (p @ [ k2 ])) x = k1 \<otimes> x \<oplus> k2"
         using eval_append_aux[of p k2 x] eval_normalize[of "p @ [ k2 ]" x] assms(2) p(3) by auto
-      thus ?case
-        using normalize_gives_polynomial[of "p @ [ k2 ]"] polynomial_incl[OF p(2)] lin(2)
+      moreover have "set (p @ [k2]) \<subseteq> K"
+        using polynomial_incl[OF p(2)] \<open>k2 \<in> K\<close> by auto
+      then have "local.normalize (p @ [k2]) \<in> carrier (K [X])"
+        using normalize_gives_polynomial univ_poly_carrier by blast
+      ultimately show ?case
         unfolding univ_poly_carrier by force
     qed
   qed
@@ -720,91 +723,4 @@
   qed
 qed
 
-
-(*
-proposition (in domain) finite_extension_is_subfield:
-  assumes "subfield K R" "set xs \<subseteq> carrier R"
-  shows "subfield (finite_extension K xs) R \<longleftrightarrow> (algebraic_set over K) (set xs)"
-proof
-  have "(\<And>x. x \<in> set xs \<Longrightarrow> (algebraic over K) x) \<Longrightarrow> subfield (finite_extension K xs) R"
-    using simple_extension_is_subfield algebraic_mono assms
-    by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1))
-  thus "(algebraic_set over K) (set xs) \<Longrightarrow> subfield (finite_extension K xs) R"
-    unfolding algebraic_set_def over_def by auto
-next
-  { fix x xs
-    assume x: "x \<in> carrier R" and xs: "set xs \<subseteq> carrier R"
-      and is_subfield: "subfield (finite_extension K (x # xs)) R"
-    hence "(algebraic over K) x" sorry }
-
-  assume "subfield (finite_extension K xs) R" thus "(algebraic_set over K) (set xs)"
-    using assms(2)
-  proof (induct xs)
-    case Nil thus ?case
-      unfolding algebraic_set_def over_def by simp
-  next
-    case (Cons x xs)
-    have "(algebraic over K) x"
-      using simple_extension_subfield_imp_algebraic[OF 
-            finite_extension_is_subring[of K xs], of x]
-
-    then show ?case sorry
-  qed
-qed
-*)
-
-(*
-lemma (in ring) transcendental_imp_trivial_ker:
-  assumes "x \<in> carrier R"
-  shows "(transcendental over K) x \<Longrightarrow> (\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = [])"
-proof -
-  fix p assume "(transcendental over K) x" "polynomial R p" "eval p x = \<zero>" "set p \<subseteq> K"
-  moreover have "eval [] x = \<zero>" and "polynomial R []"
-    using assms zero_is_polynomial by auto
-  ultimately show "p = []"
-    unfolding over_def transcendental_def inj_on_def by auto
-qed
-
-lemma (in domain) trivial_ker_imp_transcendental:
-  assumes "subring K R" and "x \<in> carrier R"
-  shows "(\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []) \<Longrightarrow> (transcendental over K) x"
-proof -
-  assume "\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []"
-  hence "a_kernel (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. local.eval p x) = { [] }"
-    unfolding a_kernel_def' univ_poly_subring_def'[OF assms(1)] by auto
-  moreover have "[] = \<zero>\<^bsub>(univ_poly (R \<lparr> carrier := K \<rparr>))\<^esub>"
-    unfolding univ_poly_def by auto
-  ultimately have "inj_on (\<lambda>p. local.eval p x) (carrier (univ_poly (R \<lparr> carrier := K \<rparr>)))"
-    using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]] by auto
-  thus "(transcendental over K) x"
-    unfolding over_def transcendental_def univ_poly_subring_def'[OF assms(1)] by simp
-qed
-
-lemma (in ring) non_trivial_ker_imp_algebraic:
-  assumes "x \<in> carrier R"
-    and "p \<noteq> []" "polynomial R p" "set p \<subseteq> K" "eval p x = \<zero>"
-  shows "(algebraic over K) x"
-  using transcendental_imp_trivial_ker[OF assms(1) _ assms(3-5)] assms(2)
-  unfolding over_def algebraic_def by auto
-
-lemma (in domain) algebraic_imp_non_trivial_ker:
-  assumes "subring K R" "x \<in> carrier R"
-  shows "(algebraic over K) x \<Longrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
-  using trivial_ker_imp_transcendental[OF assms]
-  unfolding over_def algebraic_def by auto
-
-lemma (in domain) algebraic_iff:
-  assumes "subring K R" "x \<in> carrier R"
-  shows "(algebraic over K) x \<longleftrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
-  using non_trivial_ker_imp_algebraic[OF assms(2)] algebraic_imp_non_trivial_ker[OF assms] by auto
-*)
-
-
-(*
-lemma (in field)
-  assumes "subfield K R"
-  shows "subfield (simple_extension K x) R \<longleftrightarrow> (algebraic over K) x"
-  sorry
-
-*)
 end
\ No newline at end of file
diff -r 58191e01f0b1 -r 8371a25ca177 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Tue Apr 30 11:57:45 2019 +0100
@@ -193,7 +193,7 @@
 qed
 
 
-subsection \<open>General Ideal Properies\<close>
+subsection \<open>General Ideal Properties\<close>
 
 lemma (in ideal) one_imp_carrier:
   assumes I_one_closed: "\<one> \<in> I"
@@ -210,6 +210,30 @@
   shows "i \<in> carrier R"
   using iI by (rule a_Hcarr)
 
+lemma (in ring) quotient_eq_iff_same_a_r_cos:
+  assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
+  shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
+proof
+  assume "I +> a = I +> b"
+  then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
+    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
+    unfolding a_r_coset_def' by blast
+  hence "a \<ominus> b = i"
+    using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
+  with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
+    by simp
+next
+  assume "a \<ominus> b \<in> I"
+  then obtain i where "i \<in> I" and "a = i \<oplus> b"
+    using ideal.Icarr[OF assms(1)] assms(2-3)
+    by (metis a_minus_def add.inv_solve_right)
+  hence "I +> a = (I +> i) +> b"
+    using ideal.Icarr[OF assms(1)] assms(3)
+    by (simp add: a_coset_add_assoc subsetI)
+  with \<open>i \<in> I\<close> show "I +> a = I +> b"
+    using a_rcos_zero[OF assms(1)] by simp
+qed
+
 
 subsection \<open>Intersection of Ideals\<close>
 
diff -r 58191e01f0b1 -r 8371a25ca177 src/HOL/Algebra/Polynomial_Divisibility.thy
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy	Mon Apr 29 17:11:26 2019 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy	Tue Apr 30 11:57:45 2019 +0100
@@ -122,6 +122,11 @@
   using field.univ_poly_carrier_units[OF subfield_iff(2)[OF assms]]
         univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto
 
+lemma (in domain) univ_poly_units':
+  assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
+  unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
+  by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
+
 corollary (in domain) rupture_one_not_zero:
   assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p > 0"
   shows "\<one>\<^bsub>Rupt K p\<^esub> \<noteq> \<zero>\<^bsub>Rupt K p\<^esub>"
@@ -759,6 +764,255 @@
     using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp
 qed
 
+lemma (in ring) divides_pirreducible_condition:
+  assumes "pirreducible K q" and "p \<in> carrier (K[X])"
+  shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
+  using divides_irreducible_condition[of "K[X]" q p] assms
+  unfolding ring_irreducible_def by auto
+
+subsection \<open>Polynomial Power\<close>
+
+lemma (in domain) polynomial_pow_not_zero:
+  assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
+  shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  from assms UP.integral show ?thesis
+    unfolding sym[OF univ_poly_zero[of R "carrier R"]]
+    by (induction n, auto)
+qed
+
+lemma (in domain) subring_polynomial_pow_not_zero:
+  assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
+  shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
+  using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
+  unfolding univ_poly_consistent[OF assms(1)] by simp
+
+lemma (in domain) polynomial_pow_degree:
+  assumes "p \<in> carrier (poly_ring R)"
+  shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  show ?thesis
+  proof (induction n)
+    case 0 thus ?case
+      using UP.nat_pow_0 unfolding univ_poly_one by auto
+  next
+    let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
+    case (Suc n) thus ?case
+    proof (cases "p = []")
+      case True thus ?thesis
+        using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
+    next
+      case False
+      hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
+        using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
+      thus ?thesis
+        using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
+        unfolding univ_poly_carrier univ_poly_zero
+        by (auto simp add: add.commute univ_poly_mult)
+    qed
+  qed
+qed
+
+lemma (in domain) subring_polynomial_pow_degree:
+  assumes "subring K R" and "p \<in> carrier (K[X])"
+  shows "degree (p [^]\<^bsub>K[X]\<^esub> n) = n * degree p"
+  using domain.polynomial_pow_degree[OF subring_is_domain, of K p n] assms
+  unfolding univ_poly_consistent[OF assms(1)] by simp
+
+lemma (in domain) polynomial_pow_division:
+  assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
+  shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
+
+  have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
+    using assms(1) by (simp add: UP.nat_pow_mult)
+  thus ?thesis
+    using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
+    unfolding pdivides_def by auto
+qed
+
+lemma (in domain) subring_polynomial_pow_division:
+  assumes "subring K R" and "p \<in> carrier (K[X])" and "(n::nat) \<le> m"
+  shows "(p [^]\<^bsub>K[X]\<^esub> n) divides\<^bsub>K[X]\<^esub> (p [^]\<^bsub>K[X]\<^esub> m)"
+  using domain.polynomial_pow_division[OF subring_is_domain, of K p n m] assms
+  unfolding univ_poly_consistent[OF assms(1)] pdivides_def by simp
+
+lemma (in domain) pirreducible_pow_pdivides_iff:
+  assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
+    and "pirreducible K p" and "\<not> (p pdivides q)"
+  shows "(p [^]\<^bsub>K[X]\<^esub> (n :: nat)) pdivides (q \<otimes>\<^bsub>K[X]\<^esub> r) \<longleftrightarrow> (p [^]\<^bsub>K[X]\<^esub> n) pdivides r"
+proof -
+  interpret UP: principal_domain "K[X]"
+    using univ_poly_is_principal[OF assms(1)] .
+  show ?thesis
+  proof (cases "r = []")
+    case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
+      unfolding  sym[OF univ_poly_zero[of R K]] by auto
+    thus ?thesis
+      using pdivides_zero[OF subfieldE(1),of K] assms by auto
+  next
+    case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
+      using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
+            UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
+    from \<open>p \<noteq> []\<close>
+    have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
+      using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
+    have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
+      using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
+    have prime: "prime (mult_of (K[X])) p"
+      using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
+      unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
+    have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
+      if "a \<in> carrier (K[X])" "a \<noteq> \<zero>\<^bsub>K[X]\<^esub>" "b \<in> carrier (K[X])" "b \<noteq> \<zero>\<^bsub>K[X]\<^esub>" for a b
+      using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
+      unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
+    thus ?thesis
+      using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
+      unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
+      by (metis DiffI UP.m_closed singletonD)
+  qed
+qed
+
+lemma (in domain) subring_degree_one_imp_pirreducible:
+  assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
+  shows "pirreducible K [ a, b ]"
+proof (rule pirreducibleI[OF assms(1)])
+  have "a \<in> K" and "a \<noteq> \<zero>"
+    using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
+  thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
+    using univ_poly_units_incl[OF assms(1)] assms(2-3)
+    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+next
+  interpret UP: domain "K[X]"
+    using univ_poly_is_domain[OF assms(1)] .
+
+  { fix q r
+    assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
+    hence not_zero: "q \<noteq> []" "r \<noteq> []"
+      by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
+    have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
+      using not_zero poly_mult_degree_eq[OF assms(1)] q r
+      by (simp add: univ_poly_carrier univ_poly_mult)
+    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
+      using not_zero by auto
+  } note aux_lemma1 = this
+
+  { fix q r
+    assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
+      and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
+    hence "length q = Suc (Suc 0)" and "length r = Suc 0"
+      by (linarith, metis add.right_neutral add_eq_if length_0_conv)
+    from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
+      by (metis length_0_conv length_Cons list.exhaust nat.inject)
+    from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
+      by (metis length_0_conv length_Suc_conv)
+    from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
+    have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
+      using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
+      using poly_mult_lead_coeff[OF assms(1), of q r]
+      unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
+    obtain inv_a where a: "a \<in> K" and inv_a: "inv_a \<in> K" "a \<otimes> inv_a = \<one>" "inv_a \<otimes> a = \<one>"
+      using assms(2) unfolding Units_def by auto
+    hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
+      using subringE(1)[OF assms(1)] integral_iff by auto
+    with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
+      using subringE(1,6)[OF assms(1)] inv_a integral
+      unfolding sym[OF univ_poly_carrier] polynomial_def
+      by (auto, meson subsetD)
+    moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
+      using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
+      unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
+    ultimately have "r \<in> Units (K[X])"
+      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
+  } note aux_lemma2 = this
+
+  fix q r
+  assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and qr: "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
+  thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
+    using aux_lemma1[OF q r qr] aux_lemma2[of q r] aux_lemma2[of r q] UP.m_comm add_is_1 by auto
+qed
+
+lemma (in domain) degree_one_imp_pirreducible:
+  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
+  shows "pirreducible K p"
+proof -
+  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+    by simp
+  then obtain a b where p: "p = [ a, b ]"
+    by (metis length_0_conv length_Suc_conv)
+  with \<open>p \<in> carrier (K[X])\<close> show ?thesis
+    using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
+          subfield.subfield_Units[OF assms(1)]
+    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+qed
+
+lemma (in ring) degree_oneE[elim]:
+  assumes "p \<in> carrier (K[X])" and "degree p = 1"
+    and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
+  shows P
+proof -
+  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+    by simp
+  then obtain a b where "p = [ a, b ]"
+    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
+  with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
+    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+  with \<open>p = [ a, b ]\<close> show ?thesis
+    using assms(3) by simp
+qed
+
+lemma (in domain) subring_degree_one_associatedI:
+  assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
+  shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
+proof -
+  from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
+    using subringE(1)[OF assms(1)] assms(2-3) by auto
+  hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
+    using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
+    unfolding univ_poly_mult by fastforce
+  moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
+    using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
+    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+  moreover have "[ a ] \<in> Units (K[X])"
+  proof -
+    from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
+      using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+    moreover have "a' \<otimes> a = \<one>"
+      using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp 
+    hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
+      using assms unfolding univ_poly_mult by auto
+    ultimately show ?thesis
+      unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
+  qed
+  ultimately show ?thesis
+    using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
+qed
+
+lemma (in domain) degree_one_associatedI:
+  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
+  shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
+proof -
+  from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
+  obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
+    by auto
+  thus ?thesis
+    using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
+          subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
+    unfolding const_term_def
+    by auto
+qed
+
 subsection \<open>Ideals\<close>
 
 lemma (in domain) exists_unique_gen:
@@ -882,6 +1136,26 @@
 
 subsection \<open>Roots and Multiplicity\<close>
 
+definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
+
+definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
+  where "alg_mult p x =
+           (if p = [] then 0 else
+             (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
+
+definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
+  where "roots p = Abs_multiset (alg_mult p)"
+
+definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
+  where "roots_on K p = roots p \<inter># mset_set K"
+
+definition (in ring) splitted :: "'a list \<Rightarrow> bool"
+  where "splitted p \<longleftrightarrow> size (roots p) = degree p"
+
+definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
+
 lemma (in domain) pdivides_imp_root_sharing:
   assumes "p \<in> carrier (poly_ring R)" "p pdivides q" and "a \<in> carrier R"
   shows "eval p a = \<zero> \<Longrightarrow> eval q a = \<zero>"
@@ -922,6 +1196,782 @@
   show "inv (lead_coeff p) \<otimes> (const_term p) \<in> K"
     using p subringE(6)[OF subfieldE(1)[OF assms(1)]] unfolding ct by auto
 qed
+lemma (in domain) is_root_imp_pdivides:
+  assumes "p \<in> carrier (poly_ring R)"
+  shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
+proof -
+  let ?b = "[ \<one> , \<ominus> x ]"
+
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
+    unfolding is_root_def by auto
+  hence b: "?b \<in> carrier (poly_ring R)"
+    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+  then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
+    and long_divides: "p = (?b \<otimes>\<^bsub>poly_ring R\<^esub> q) \<oplus>\<^bsub>poly_ring R\<^esub> r" "r = [] \<or> degree r < degree ?b"
+    using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
+
+  show ?thesis
+  proof (cases "r = []")
+    case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
+      unfolding univ_poly_zero[of R "carrier R"] .
+    thus ?thesis
+      using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
+  next
+    case False then have "length r = Suc 0"
+      using long_divides(2) le_SucE by fastforce
+    then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
+      using r unfolding sym[OF univ_poly_carrier] polynomial_def
+      by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
+
+    have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
+      using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
+    also have " ... = eval r x"
+      using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
+    finally have "a = \<zero>"
+      using a unfolding \<open>r = [ a ]\<close> is_root by simp
+    with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
+  qed
+qed
+
+lemma (in domain) pdivides_imp_is_root:
+  assumes "p \<noteq> []" and "x \<in> carrier R"
+  shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
+proof -
+  assume "[ \<one>, \<ominus> x ] pdivides p"
+  then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
+    unfolding pdivides_def by auto
+  moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+  ultimately have "eval p x = \<zero>"
+    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
+  with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
+    unfolding is_root_def by simp 
+qed
+
+lemma (in domain) associated_polynomials_imp_same_is_root:
+  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+  shows "is_root p x \<longleftrightarrow> is_root q x"
+proof (cases "p = []")
+  case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
+    unfolding associated_def True factor_def univ_poly_def by auto
+  thus ?thesis
+    using True unfolding is_root_def by simp 
+next
+  case False
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  { fix p q
+    assume p: "p \<in> carrier (poly_ring R)" and q: "q \<in> carrier (poly_ring R)" and pq: "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+    have "is_root p x \<Longrightarrow> is_root q x"
+    proof -
+      assume is_root: "is_root p x"
+      then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
+        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
+      moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
+      ultimately have "[ \<one>, \<ominus> x ] pdivides q"
+        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
+      with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
+        using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
+              pdivides_imp_is_root[of q x]
+        by fastforce  
+    qed
+  }
+
+  then show ?thesis
+    using assms UP.associated_sym[OF assms(3)] by blast 
+qed
+
+lemma (in ring) monic_degree_one_root_condition:
+  assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
+  using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
+
+lemma (in field) degree_one_root_condition:
+  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
+  shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
+    by simp
+  then obtain a b where p: "p = [ a, b ]"
+    by (metis length_0_conv length_Cons list.exhaust nat.inject)
+  hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
+    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+  hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
+    using subfield_m_inv[OF carrier_is_subfield, of a] by auto
+  hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
+    using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+
+  have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
+  proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
+    have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
+      using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
+    also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
+      using UP.m_comm[OF in_carrier, of "[ a ]"] a
+      by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
+    finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
+  next
+    from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
+      unfolding univ_poly_units[OF carrier_is_subfield] by simp
+  qed
+
+  moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
+    and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
+    using inv_a a b unfolding p const_term_def by auto
+
+  ultimately show ?thesis
+    using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
+          monic_degree_one_root_condition
+    by (metis add.inv_closed)
+qed
+
+lemma (in domain) is_root_poly_mult_imp_is_root:
+  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
+  shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
+  hence "p \<noteq> []" and "q \<noteq> []"
+    unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
+    using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
+  moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
+    using is_root unfolding is_root_def by simp+
+  hence "eval p x = \<zero> \<or> eval q x = \<zero>"
+    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto 
+  ultimately show "(is_root p x) \<or> (is_root q x)"
+    using x unfolding is_root_def by auto
+qed
+
+lemma (in domain) degree_zero_imp_not_is_root:
+  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
+proof (cases "p = []", simp add: is_root_def)
+  case False with \<open>degree p = 0\<close> have "length p = Suc 0"
+    using le_SucE by fastforce 
+  then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
+    using assms unfolding sym[OF univ_poly_carrier] polynomial_def
+    by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
+  thus ?thesis
+    unfolding is_root_def by auto 
+qed
+
+lemma (in domain) finite_number_of_roots:
+  assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
+  using assms
+proof (induction "degree p" arbitrary: p)
+  case 0 thus ?case
+    by (simp add: degree_zero_imp_not_is_root)
+next
+  case (Suc n) show ?case
+  proof (cases "{ x. is_root p x } = {}")
+    case True thus ?thesis
+      by (simp add: True) 
+  next
+    interpret UP: domain "poly_ring R"
+      using univ_poly_is_domain[OF carrier_is_subring] .
+
+    case False
+    then obtain a where is_root: "is_root p a"
+      by blast
+    hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
+      unfolding is_root_def by auto
+    hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+
+    obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
+      using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
+    with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
+      using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
+      by metis
+    hence "degree q = n"
+      using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
+            in_carrier q p_not_zero p Suc(2)
+      unfolding univ_poly_carrier
+      by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
+                list.size(3-4) plus_1_eq_Suc univ_poly_mult)
+    hence "finite { x. is_root q x }"
+      using Suc(1)[OF _ q] by simp
+
+    moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
+      using is_root_poly_mult_imp_is_root[OF in_carrier q]
+            monic_degree_one_root_condition[OF a]
+      unfolding p by auto
+
+    ultimately show ?thesis
+      using finite_subset by auto
+  qed
+qed
+
+lemma (in domain) alg_multE:
+  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
+  shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
+    and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
+
+  define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
+  have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
+    using UP.nat_pow_0 by simp
+  hence "0 \<in> S"
+    using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
+  hence "S \<noteq> {}"
+    by auto
+
+  moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
+  proof -
+    have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+      using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+    hence "?ppow n \<in> carrier (poly_ring R)"
+      using assms unfolding univ_poly_zero by auto
+    with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
+      using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
+    with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
+      using polynomial_pow_degree by simp
+  qed
+  hence "finite S"
+    using finite_nat_set_iff_bounded_le by blast
+
+  ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
+    using Max_ge[of S] Max_in[of S] by auto
+  with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
+    using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
+    unfolding S_def alg_mult_def by auto
+  thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
+   and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
+    using MaxS unfolding S_def by auto
+qed
+
+lemma (in domain) le_alg_mult_imp_pdivides:
+  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
+  shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  assume le_alg_mult: "n \<le> alg_mult p x"
+  have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+  hence ppow_pdivides:
+    "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
+     ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
+    using polynomial_pow_division[OF _ le_alg_mult] by simp
+
+  show ?thesis
+  proof (cases "p = []")
+    case True thus ?thesis
+      using in_carrier pdivides_zero[OF carrier_is_subring] by auto
+  next
+    case False thus ?thesis
+      using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
+      unfolding pdivides_def by meson
+  qed
+qed
+
+lemma (in domain) alg_mult_gt_zero_iff_is_root:
+  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+  show ?thesis
+  proof
+    assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
+      unfolding is_root_def by auto
+    have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
+      using x unfolding univ_poly_def by auto
+    thus "alg_mult p x > 0"
+      using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
+  next
+    assume gt_zero: "alg_mult p x > 0"
+    hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
+      unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
+    hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
+      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+    with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
+      using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
+    thus "is_root p x"
+      using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
+  qed
+qed
+
+lemma (in domain) alg_mult_eq_count_roots:
+  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
+  using finite_number_of_roots[OF assms]
+  unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
+  by (simp add: multiset_def roots_def) 
+
+lemma (in domain) roots_mem_iff_is_root:
+  assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
+  using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
+  unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
+
+lemma (in domain) degree_zero_imp_empty_roots:
+  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
+  using degree_zero_imp_not_is_root[of p] roots_mem_iff_is_root[of p] assms by auto
+
+lemma (in domain) degree_zero_imp_splitted:
+  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
+  unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
+
+lemma (in domain) roots_inclI':
+  assumes "p \<in> carrier (poly_ring R)" and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> alg_mult p a \<le> count m a" 
+  shows "roots p \<subseteq># m"
+proof (intro mset_subset_eqI)
+  fix a show "count (roots p) a \<le> count m a"
+    using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
+    by (cases "p = []", simp, cases "a \<in> carrier R", auto)
+qed
+
+lemma (in domain) roots_inclI:
+  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+    and "\<And>a. \<lbrakk> a \<in> carrier R; p \<noteq> [] \<rbrakk> \<Longrightarrow> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
+  shows "roots p \<subseteq># roots q"
+  using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
+  unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
+
+lemma (in domain) pdivides_imp_roots_incl:
+  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+  shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
+proof (rule roots_inclI[OF assms])
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  fix a assume "p pdivides q" and a: "a \<in> carrier R"
+  hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
+    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+  with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
+    using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
+    by (auto simp add: pdivides_def)
+qed
+
+lemma (in domain) associated_polynomials_imp_same_roots:
+  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
+  shows "roots p = roots q"
+  using assms pdivides_imp_roots_incl zero_pdivides
+  unfolding pdivides_def associated_def 
+  by (metis subset_mset.eq_iff)
+
+lemma (in domain) monic_degree_one_roots:
+  assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
+proof -
+  let ?p = "[ \<one> , \<ominus> a ]"
+
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
+    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+  show ?thesis
+  proof (rule subset_mset.antisym)
+    show "{# a #} \<subseteq># roots ?p"
+      using roots_mem_iff_is_root[OF in_carrier]
+            monic_degree_one_root_condition[OF assms]
+      by simp
+  next
+    show "roots ?p \<subseteq># {# a #}"
+    proof (rule mset_subset_eqI, auto)
+      fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
+        using alg_mult_gt_zero_iff_is_root[OF in_carrier]
+              monic_degree_one_root_condition[OF assms]
+        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
+        by fastforce
+    next
+      have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
+        using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
+      hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
+        using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
+      thus "count (roots ?p) a \<le> Suc 0"
+        using polynomial_pow_degree[OF in_carrier]
+        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
+        by auto
+    qed
+  qed
+qed
+
+lemma (in domain) degree_one_roots:
+  assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
+  shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
+proof -
+  have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
+    using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+  thus ?thesis
+    using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
+          monic_degree_one_roots associated_polynomials_imp_same_roots
+    by (metis add.inv_closed local.minus_minus m_closed)
+qed
+
+lemma (in field) degree_one_imp_singleton_roots:
+  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
+  shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
+proof -
+  from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
+  obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
+    by auto
+  thus ?thesis
+    using degree_one_roots[of a "inv a" b]
+    by (auto simp add: const_term_def field_Units)
+qed
+
+lemma (in field) degree_one_imp_splitted:
+  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
+  using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
+
+lemma (in field) no_roots_imp_same_roots:
+  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
+  shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+
+  assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+  proof (intro subset_mset.antisym)
+    have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+      using UP.divides_prod_l assms unfolding pdivides_def by blast
+    show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+      using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
+            degree_zero_imp_empty_roots[OF assms(3)]
+      by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
+  next
+    show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
+    proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
+      case True thus ?thesis
+        using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
+    next
+      case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
+        by (metis UP.r_null assms(1) univ_poly_zero)
+      show ?thesis
+      proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
+        fix a assume a: "a \<in> carrier R"
+        hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
+          using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
+        moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+          using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+        hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
+          using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
+        moreover
+        have "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+          using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
+        ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
+          using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
+      qed
+    qed
+  qed
+qed
+
+lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
+  assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
+  shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+  
+  from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+
+  show ?thesis
+  proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
+    show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
+      using in_carrier assms(2) by simp
+  next
+    fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
+    hence not_zero: "p \<noteq> []"
+      unfolding univ_poly_def by auto
+    from \<open>b \<in> carrier R\<close> have in_carrier':  "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
+      unfolding sym[OF univ_poly_carrier] polynomial_def by simp
+    show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
+    proof (cases "a = b")
+      case False
+      hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
+        using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
+      moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
+        using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
+      ultimately
+      have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
+        using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
+              pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
+        by auto
+      with \<open>a \<noteq> b\<close> show ?thesis
+        using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
+    next
+      case True
+      have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+        using dividesI[OF assms(2)] unfolding pdivides_def by auto
+      with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
+      have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
+        using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
+      then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
+        using Suc_le_D by blast
+      hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
+             ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+        using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
+              in_carrier assms UP.nat_pow_Suc2 by force
+      hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
+        using UP.mult_divides in_carrier assms(2)
+        unfolding univ_poly_zero pdivides_def factor_def
+        by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
+      with \<open>a = b\<close> show ?thesis
+        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2 
+              alg_multE(2)[OF assms(1) _ not_zero] m
+        by auto
+    qed
+  next
+    fix b
+    have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
+      using assms in_carrier univ_poly_zero[of R] UP.integral by auto
+
+    show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
+    proof (cases "a = b")
+      case True
+      have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
+            ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+        using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
+        by (auto simp add: pdivides_def)
+      with \<open>a = b\<close> show ?thesis
+        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2 
+              alg_multE(2)[OF assms(1) _ not_zero]
+        by auto
+    next
+      case False
+      have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
+        using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
+      thus ?thesis
+        using False pdivides_imp_roots_incl assms in_carrier not_zero
+        by (simp add: subseteq_mset_def)
+    qed
+  qed
+qed
+
+lemma (in domain) not_empty_rootsE[elim]:
+  assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
+    and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
+               [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
+  shows P
+proof -
+  from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
+    by blast
+  with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
+    and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
+    using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
+    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
+  with \<open>a \<in># roots p\<close> show ?thesis
+    using assms(3)[of a] by auto
+qed
+
+lemma (in field) associated_polynomials_imp_same_roots:
+  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
+  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots p + roots q"
+proof -
+  interpret UP: domain "poly_ring R"
+    using univ_poly_is_domain[OF carrier_is_subring] .
+  from assms show ?thesis
+  proof (induction "degree p" arbitrary: p rule: less_induct)
+    case less show ?case
+    proof (cases "roots p = {#}")
+      case True thus ?thesis
+        using no_roots_imp_same_roots[of p q] less by simp
+    next
+      case False with \<open>p \<in> carrier (poly_ring R)\<close>
+      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
+          and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+        by blast
+      show ?thesis
+      proof (cases "degree p = 1")
+        case True with \<open>p \<in> carrier (poly_ring R)\<close>
+        obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
+          by auto
+        with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
+          and lead: "lead_coeff p = b" and const: "const_term p = c"
+          using degree_one_imp_singleton_roots[of p] less(2) field_Units
+          unfolding const_term_def by auto
+        hence "(p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<sim>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+          using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
+          by (auto simp add: a lead const)
+        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
+          using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
+        thus ?thesis
+          unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
+      next
+        case False
+        from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
+        obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
+          unfolding pdivides_def by auto
+        with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
+          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
+        with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
+          using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
+          unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+        with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
+          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
+        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
+          using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
+                UP.m_assoc[OF in_carrier r less(4)] p by auto
+        also have " ... = add_mset a (roots r + roots q)"
+          using less(1)[OF _ r not_zero less(4-5)] deg by simp
+        also have " ... = (add_mset a (roots r)) + roots q"
+          by simp
+        also have " ... = roots p + roots q"
+          using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp 
+        finally show ?thesis .
+      qed
+    qed
+  qed
+qed
+
+lemma (in field) size_roots_le_degree:
+  assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
+  using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+  case less show ?case
+  proof (cases "roots p = {#}", simp)
+    interpret UP: domain "poly_ring R"
+      using univ_poly_is_domain[OF carrier_is_subring] .
+
+    case False with \<open>p \<in> carrier (poly_ring R)\<close>
+    obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+      and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+      by blast
+    then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
+      unfolding pdivides_def by auto
+    with \<open>a \<in># roots p\<close> have "p \<noteq> []"
+      using degree_zero_imp_empty_roots[OF less(2)] by auto
+    hence not_zero: "q \<noteq> []"
+      using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
+    hence "degree p = Suc (degree q)"
+      using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
+      unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+    with \<open>q \<noteq> []\<close> show ?thesis
+      using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
+      by (metis Suc_le_mono lessI size_add_mset) 
+  qed
+qed
+
+lemma (in domain) pirreducible_roots:
+  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+  shows "roots p = {#}"
+proof (rule ccontr)
+  assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
+  obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+    and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+    by blast
+  hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
+    using divides_pirreducible_condition[OF assms(2) in_carrier]
+          univ_poly_units_incl[OF carrier_is_subring]
+    unfolding pdivides_def by auto
+  hence "degree p = 1"
+    using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
+  with \<open>degree p \<noteq> 1\<close> show False ..
+qed
+
+lemma (in field) pirreducible_imp_not_splitted:
+  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+  shows "\<not> splitted p"
+  using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
+  by (simp add: splitted_def)
+
+lemma (in field)
+  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
+    and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
+  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
+  using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
+  unfolding ring_irreducible_def univ_poly_zero by auto
+
+lemma (in field) trivial_factors_imp_splitted:
+  assumes "p \<in> carrier (poly_ring R)"
+    and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
+  shows "splitted p"
+  using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+  interpret UP: principal_domain "poly_ring R"
+    using univ_poly_is_principal[OF carrier_is_subfield] .
+  case less show ?case
+  proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
+    case False show ?thesis
+    proof (cases "roots p = {#}")
+      case True
+      from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
+        using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
+      then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
+        using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
+      with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
+        using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
+              pdivides_imp_roots_incl[OF _ less(2), of q]
+              pirreducible_degree[OF carrier_is_subfield, of q]
+        by force
+      from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
+        by simp
+      thus ?thesis ..
+    next
+      case False with \<open>p \<in> carrier (poly_ring R)\<close>
+      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
+        and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
+        by blast
+      then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
+        unfolding pdivides_def by blast
+      with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
+        by auto
+      with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
+        using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
+      with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> and \<open>p \<noteq> []\<close> have "degree p = Suc (degree q)"
+        using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
+        unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
+      moreover have "q pdivides p"
+        using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
+      hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
+        and "r pdivides q" for r
+        using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
+              pirreducible_degree[OF carrier_is_subfield that(1-2)] 
+        by (auto simp add: pdivides_def)
+      ultimately have "splitted q"
+        using less(1)[OF _ q] by auto
+      with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
+        using poly_mult_degree_one_monic_imp_same_roots[OF a q]
+        unfolding sym[OF p] splitted_def
+        by simp
+    qed
+  qed
+qed
+
+lemma (in field) pdivides_imp_splitted:
+  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q" 
+  shows "p pdivides q \<Longrightarrow> splitted p"
+proof (cases "p = []")
+  case True thus ?thesis
+    using degree_zero_imp_splitted[OF assms(1)] by simp
+next
+  interpret UP: principal_domain "poly_ring R"
+    using univ_poly_is_principal[OF carrier_is_subfield] .
+
+  case False
+  assume "p pdivides q"
+  then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
+    unfolding pdivides_def by auto
+  with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
+    using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
+  hence "degree p + degree b = size (roots p) + size (roots b)"
+    using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
+          poly_mult_degree_eq[OF carrier_is_subring,of p b]
+    unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
+    by auto
+  moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
+    using size_roots_le_degree assms(1) b by auto
+  ultimately show ?thesis
+    unfolding splitted_def by linarith
+qed
+
+lemma (in field) splitted_imp_trivial_factors:
+  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
+  shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
+  using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
+  by auto 
 
 
 subsection \<open>Link between @{term \<open>(pmod)\<close>} and @{term rupture_surj}\<close>
@@ -970,32 +2020,6 @@
   qed
 qed
 
-(* Move to Ideal.thy ========================================================= *)
-lemma (in ring) quotient_eq_iff_same_a_r_cos:
-  assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
-  shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
-proof
-  assume "I +> a = I +> b"
-  then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
-    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
-    unfolding a_r_coset_def' by blast
-  hence "a \<ominus> b = i"
-    using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
-  with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
-    by simp
-next
-  assume "a \<ominus> b \<in> I"
-  then obtain i where "i \<in> I" and "a = i \<oplus> b"
-    using ideal.Icarr[OF assms(1)] assms(2-3)
-    by (metis a_minus_def add.inv_solve_right)
-  hence "I +> a = (I +> i) +> b"
-    using ideal.Icarr[OF assms(1)] assms(3)
-    by (simp add: a_coset_add_assoc subsetI)
-  with \<open>i \<in> I\<close> show "I +> a = I +> b"
-    using a_rcos_zero[OF assms(1)] by simp
-qed
-(* ========================================================================== *)
-
 lemma (in domain) rupture_surj_inj_on:
   assumes "subfield K R" and "p \<in> carrier (K[X])"
   shows "inj_on (rupture_surj K p) ((\<lambda>q. q pmod p) ` (carrier (K[X])))"
diff -r 58191e01f0b1 -r 8371a25ca177 src/HOL/Algebra/Pred_Zorn.thy
--- a/src/HOL/Algebra/Pred_Zorn.thy	Mon Apr 29 17:11:26 2019 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-theory Pred_Zorn
-  imports HOL.Zorn
-
-begin
-
-(* ========== *)
-lemma partial_order_onE:
-  assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
-  using assms unfolding partial_order_on_def preorder_on_def by auto
-(* ========== *)
-
-abbreviation rel_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
-  where "rel_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
-
-lemma Field_rel_of:
-  assumes "refl_on A (rel_of P A)" shows "Field (rel_of P A) = A"
-  using assms unfolding refl_on_def Field_def by auto
-
-(* ========== *)
-lemma Chains_rel_of:
-  assumes "C \<in> Chains (rel_of P A)" shows "C \<subseteq> A"
-  using assms unfolding Chains_def by auto
-(* ========== *)
-
-lemma partial_order_on_rel_ofI:
-  assumes refl: "\<And>a. a \<in> A \<Longrightarrow> P a a"
-    and trans: "\<And>a b c. \<lbrakk> a \<in> A; b \<in> A; c \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b c \<Longrightarrow> P a c"
-    and antisym: "\<And>a b. \<lbrakk> a \<in> A; b \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b a \<Longrightarrow> a = b"
-  shows "partial_order_on A (rel_of P A)"
-proof -
-  from refl have "refl_on A (rel_of P A)"
-    unfolding refl_on_def by auto
-  moreover have "trans (rel_of P A)" and "antisym (rel_of P A)"
-    by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
-  ultimately show ?thesis
-    unfolding partial_order_on_def preorder_on_def by simp
-qed
-
-lemma Partial_order_rel_ofI:
-  assumes "partial_order_on A (rel_of P A)" shows "Partial_order (rel_of P A)"
-  using assms unfolding Field_rel_of[OF partial_order_onE(1)[OF assms]] .
-
-lemma predicate_Zorn:
-  assumes "partial_order_on A (rel_of P A)"
-    and "\<forall>C \<in> Chains (rel_of P A). \<exists>u \<in> A. \<forall>a \<in> C. P a u"
-  shows "\<exists>m \<in> A. \<forall>a \<in> A. P m a \<longrightarrow> a = m"
-proof -
-  have "a \<in> A" if "a \<in> C" and "C \<in> Chains (rel_of P A)" for C a
-    using that Chains_rel_of by auto
-  moreover have "(a, u) \<in> rel_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u
-    using that by auto
-  ultimately show ?thesis
-    using Zorns_po_lemma[OF Partial_order_rel_ofI[OF assms(1)]] assms(2)
-    unfolding Field_rel_of[OF partial_order_onE(1)[OF assms(1)]] by auto
-qed
-
-end
\ No newline at end of file