Algebraic closure: moving more theorems into their rightful places
authorpaulson <lp15@cam.ac.uk>
Tue Apr 30 11:57:45 2019 +0100 (4 months ago)
changeset 702158371a25ca177
parent 70214 58191e01f0b1
child 70216 40f19372a723
Algebraic closure: moving more theorems into their rightful places
NEWS
src/HOL/Algebra/Algebraic_Closure.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Finite_Extensions.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Polynomial_Divisibility.thy
src/HOL/Algebra/Pred_Zorn.thy
     1.1 --- a/NEWS	Mon Apr 29 17:11:26 2019 +0100
     1.2 +++ b/NEWS	Tue Apr 30 11:57:45 2019 +0100
     1.3 @@ -266,7 +266,7 @@
     1.4  at the level of abstract topological spaces.
     1.5  
     1.6  * Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
     1.7 -proofs towards algebraic closure by de Vilhena and Baillon.
     1.8 + algebraic closure of a field by de Vilhena and Baillon.
     1.9  
    1.10  * Session HOL-Homology has been added. It is a port of HOL Light's
    1.11  homology library, with new proofs of "invariance of domain" and related
     2.1 --- a/src/HOL/Algebra/Algebraic_Closure.thy	Mon Apr 29 17:11:26 2019 +0100
     2.2 +++ b/src/HOL/Algebra/Algebraic_Closure.thy	Tue Apr 30 11:57:45 2019 +0100
     2.3 @@ -61,7 +61,7 @@
     2.4  lemma (in field) law_restrict_is_field: "field (law_restrict R)"
     2.5  proof -
     2.6    have "comm_monoid_axioms (law_restrict R)"
     2.7 -    using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto
     2.8 +    using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto 
     2.9    then interpret L: cring "law_restrict R"
    2.10      using cring.intro law_restrict_is_ring comm_monoid.intro ring.is_monoid by auto
    2.11    have "Units R = Units (law_restrict R)"
    2.12 @@ -69,7 +69,7 @@
    2.13    thus ?thesis
    2.14      using L.cring_fieldI unfolding field_Units law_restrict_carrier law_restrict_zero by simp
    2.15  qed
    2.16 -
    2.17 +    
    2.18  lemma law_restrict_iso_imp_eq:
    2.19    assumes "id \<in> ring_iso (law_restrict A) (law_restrict B)" and "ring A" and "ring B"
    2.20    shows "law_restrict A = law_restrict B"
    2.21 @@ -108,33 +108,33 @@
    2.22  
    2.23  subsection \<open>Partial Order\<close>
    2.24  
    2.25 -lemma iso_incl_backwards:
    2.26 +lemma iso_incl_backwards: 
    2.27    assumes "A \<lesssim> B" shows "id \<in> ring_hom A B"
    2.28    using assms by cases
    2.29  
    2.30 -lemma iso_incl_antisym_aux:
    2.31 +lemma iso_incl_antisym_aux: 
    2.32    assumes "A \<lesssim> B" and "B \<lesssim> A" shows "id \<in> ring_iso A B"
    2.33 -proof -
    2.34 -  have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A"
    2.35 +proof - 
    2.36 +  have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A" 
    2.37      using assms(1-2)[THEN iso_incl_backwards] by auto
    2.38 -  thus ?thesis
    2.39 +  thus ?thesis 
    2.40      using hom[THEN ring_hom_memE(1)] by (auto simp add: ring_iso_def bij_betw_def inj_on_def)
    2.41  qed
    2.42  
    2.43 -lemma iso_incl_refl: "A \<lesssim> A"
    2.44 +lemma iso_incl_refl: "A \<lesssim> A" 
    2.45    by (rule iso_inclI[OF ring_hom_memI], auto)
    2.46  
    2.47 -lemma iso_incl_trans:
    2.48 +lemma iso_incl_trans: 
    2.49    assumes "A \<lesssim> B" and "B \<lesssim> C" shows "A \<lesssim> C"
    2.50    using ring_hom_trans[OF assms[THEN iso_incl_backwards]] by auto
    2.51  
    2.52  lemma (in ring) iso_incl_antisym:
    2.53    assumes "A \<in> \<S>" "B \<in> \<S>" and "A \<lesssim> B" "B \<lesssim> A" shows "A = B"
    2.54 -proof -
    2.55 -  obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
    2.56 +proof - 
    2.57 +  obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring" 
    2.58      where A: "A = law_restrict A'" "ring A'" and B: "B = law_restrict B'" "ring B'"
    2.59      using assms(1-2) field.is_ring by (auto simp add: extensions_def)
    2.60 -  thus ?thesis
    2.61 +  thus ?thesis 
    2.62      using law_restrict_iso_imp_eq iso_incl_antisym_aux[OF assms(3-4)] by simp
    2.63  qed
    2.64  
    2.65 @@ -190,7 +190,7 @@
    2.66  subsection \<open>Chains\<close>
    2.67  
    2.68  definition union_ring :: "(('a, 'c) ring_scheme) set \<Rightarrow> 'a ring"
    2.69 -  where "union_ring C =
    2.70 +  where "union_ring C = 
    2.71             \<lparr> carrier = (\<Union>(carrier ` C)),
    2.72           monoid.mult = (\<lambda>a b. (monoid.mult (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b)),
    2.73                   one = one (SOME R. R \<in> C),
    2.74 @@ -277,7 +277,7 @@
    2.75      using field_chain by simp
    2.76  
    2.77    show "a \<otimes>\<^bsub>union_ring C\<^esub> b \<in> carrier (union_ring C)"
    2.78 -    using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto
    2.79 +    using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto 
    2.80    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)"
    2.81     and "a \<otimes>\<^bsub>union_ring C\<^esub> b = b \<otimes>\<^bsub>union_ring C\<^esub> a"
    2.82     and "\<one>\<^bsub>union_ring C\<^esub> \<otimes>\<^bsub>union_ring C\<^esub> a = a"
    2.83 @@ -286,7 +286,7 @@
    2.84  next
    2.85    show "\<one>\<^bsub>union_ring C\<^esub> \<in> carrier (union_ring C)"
    2.86      using ring.ring_simprules(6)[OF ring_chain] assms same_one_same_zero(1)
    2.87 -    unfolding union_ring_carrier by auto
    2.88 +    unfolding union_ring_carrier by auto    
    2.89  qed
    2.90  
    2.91  lemma union_ring_is_abelian_group:
    2.92 @@ -304,7 +304,7 @@
    2.93    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)"
    2.94     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)"
    2.95     and "a \<oplus>\<^bsub>union_ring C\<^esub> b = b \<oplus>\<^bsub>union_ring C\<^esub> a"
    2.96 -   and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a"
    2.97 +   and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a" 
    2.98      using same_one_same_zero[OF R(1)] same_laws[OF R(1)] R(2-4) l_distr a_assoc a_comm by auto
    2.99    have "\<exists>a' \<in> carrier R. a' \<oplus>\<^bsub>union_ring C\<^esub> a = \<zero>\<^bsub>union_ring C\<^esub>"
   2.100      using same_laws(2)[OF R(1)] R(2) same_one_same_zero[OF R(1)] by simp
   2.101 @@ -330,7 +330,7 @@
   2.102        using field_chain by simp
   2.103  
   2.104      from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>\<close> have "a \<in> Units R"
   2.105 -      unfolding same_one_same_zero[OF R(1)] field_Units by auto
   2.106 +      unfolding same_one_same_zero[OF R(1)] field_Units by auto 
   2.107      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>"
   2.108        using same_laws[OF R(1)] same_one_same_zero[OF R(1)] R(2) unfolding Units_def by auto
   2.109      with \<open>R \<in> C\<close> and \<open>a \<in> carrier (union_ring C)\<close> show "a \<in> Units (union_ring C)"
   2.110 @@ -457,11 +457,11 @@
   2.111    hence "set (map h p) \<subseteq> carrier S"
   2.112      by (induct p) (auto)
   2.113    moreover have "h a = \<zero>\<^bsub>S\<^esub> \<Longrightarrow> a = \<zero>\<^bsub>R\<^esub>" if "a \<in> carrier R" for a
   2.114 -    using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp
   2.115 +    using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp 
   2.116    with \<open>set p \<subseteq> carrier R\<close> have "lead_coeff (map h p) \<noteq> \<zero>\<^bsub>S\<^esub>" if "p \<noteq> []"
   2.117      using lc[OF that] that by (cases p) (auto)
   2.118    ultimately show ?thesis
   2.119 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.120 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto 
   2.121  qed
   2.122  
   2.123  lemma (in ring_hom_ring) subfield_polynomial_hom:
   2.124 @@ -482,1147 +482,6 @@
   2.125  qed
   2.126  
   2.127  
   2.128 -(* MOVE ========== *)
   2.129 -subsection \<open>Roots and Multiplicity\<close>
   2.130 -
   2.131 -definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
   2.132 -  where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
   2.133 -
   2.134 -definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
   2.135 -  where "alg_mult p x =
   2.136 -           (if p = [] then 0 else
   2.137 -             (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
   2.138 -
   2.139 -definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
   2.140 -  where "roots p = Abs_multiset (alg_mult p)"
   2.141 -
   2.142 -definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
   2.143 -  where "roots_on K p = roots p \<inter># mset_set K"
   2.144 -
   2.145 -definition (in ring) splitted :: "'a list \<Rightarrow> bool"
   2.146 -  where "splitted p \<longleftrightarrow> size (roots p) = degree p"
   2.147 -
   2.148 -definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
   2.149 -  where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
   2.150 -
   2.151 -lemma (in domain) polynomial_pow_not_zero:
   2.152 -  assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
   2.153 -  shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
   2.154 -proof -
   2.155 -  interpret UP: domain "poly_ring R"
   2.156 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.157 -
   2.158 -  from assms UP.integral show ?thesis
   2.159 -    unfolding sym[OF univ_poly_zero[of R "carrier R"]]
   2.160 -    by (induction n, auto)
   2.161 -qed
   2.162 -
   2.163 -lemma (in domain) subring_polynomial_pow_not_zero:
   2.164 -  assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
   2.165 -  shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
   2.166 -  using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
   2.167 -  unfolding univ_poly_consistent[OF assms(1)] by simp
   2.168 -
   2.169 -lemma (in domain) polynomial_pow_degree:
   2.170 -  assumes "p \<in> carrier (poly_ring R)"
   2.171 -  shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
   2.172 -proof -
   2.173 -  interpret UP: domain "poly_ring R"
   2.174 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.175 -
   2.176 -  show ?thesis
   2.177 -  proof (induction n)
   2.178 -    case 0 thus ?case
   2.179 -      using UP.nat_pow_0 unfolding univ_poly_one by auto
   2.180 -  next
   2.181 -    let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
   2.182 -    case (Suc n) thus ?case
   2.183 -    proof (cases "p = []")
   2.184 -      case True thus ?thesis
   2.185 -        using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
   2.186 -    next
   2.187 -      case False
   2.188 -      hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
   2.189 -        using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
   2.190 -      thus ?thesis
   2.191 -        using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
   2.192 -        unfolding univ_poly_carrier univ_poly_zero
   2.193 -        by (auto simp add: add.commute univ_poly_mult)
   2.194 -    qed
   2.195 -  qed
   2.196 -qed
   2.197 -
   2.198 -lemma (in domain) polynomial_pow_division:
   2.199 -  assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
   2.200 -  shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
   2.201 -proof -
   2.202 -  interpret UP: domain "poly_ring R"
   2.203 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.204 -
   2.205 -  let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
   2.206 -
   2.207 -  have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
   2.208 -    using assms(1) by (simp add: UP.nat_pow_mult)
   2.209 -  thus ?thesis
   2.210 -    using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
   2.211 -    unfolding pdivides_def by auto
   2.212 -qed
   2.213 -
   2.214 -lemma (in domain) degree_zero_imp_not_is_root:
   2.215 -  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
   2.216 -proof (cases "p = []", simp add: is_root_def)
   2.217 -  case False with \<open>degree p = 0\<close> have "length p = Suc 0"
   2.218 -    using le_SucE by fastforce
   2.219 -  then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
   2.220 -    using assms unfolding sym[OF univ_poly_carrier] polynomial_def
   2.221 -    by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
   2.222 -  thus ?thesis
   2.223 -    unfolding is_root_def by auto
   2.224 -qed
   2.225 -
   2.226 -lemma (in domain) is_root_imp_pdivides:
   2.227 -  assumes "p \<in> carrier (poly_ring R)"
   2.228 -  shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
   2.229 -proof -
   2.230 -  let ?b = "[ \<one> , \<ominus> x ]"
   2.231 -
   2.232 -  interpret UP: domain "poly_ring R"
   2.233 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.234 -
   2.235 -  assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
   2.236 -    unfolding is_root_def by auto
   2.237 -  hence b: "?b \<in> carrier (poly_ring R)"
   2.238 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.239 -  then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
   2.240 -    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"
   2.241 -    using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
   2.242 -
   2.243 -  show ?thesis
   2.244 -  proof (cases "r = []")
   2.245 -    case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
   2.246 -      unfolding univ_poly_zero[of R "carrier R"] .
   2.247 -    thus ?thesis
   2.248 -      using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
   2.249 -  next
   2.250 -    case False then have "length r = Suc 0"
   2.251 -      using long_divides(2) le_SucE by fastforce
   2.252 -    then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
   2.253 -      using r unfolding sym[OF univ_poly_carrier] polynomial_def
   2.254 -      by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
   2.255 -
   2.256 -    have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
   2.257 -      using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
   2.258 -    also have " ... = eval r x"
   2.259 -      using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
   2.260 -    finally have "a = \<zero>"
   2.261 -      using a unfolding \<open>r = [ a ]\<close> is_root by simp
   2.262 -    with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
   2.263 -  qed
   2.264 -qed
   2.265 -
   2.266 -lemma (in domain) pdivides_imp_is_root:
   2.267 -  assumes "p \<noteq> []" and "x \<in> carrier R"
   2.268 -  shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
   2.269 -proof -
   2.270 -  assume "[ \<one>, \<ominus> x ] pdivides p"
   2.271 -  then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
   2.272 -    unfolding pdivides_def by auto
   2.273 -  moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   2.274 -    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   2.275 -  ultimately have "eval p x = \<zero>"
   2.276 -    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
   2.277 -  with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
   2.278 -    unfolding is_root_def by simp
   2.279 -qed
   2.280 -
   2.281 -lemma (in domain) associated_polynomials_imp_same_is_root:
   2.282 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
   2.283 -  shows "is_root p x \<longleftrightarrow> is_root q x"
   2.284 -proof (cases "p = []")
   2.285 -  case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
   2.286 -    unfolding associated_def True factor_def univ_poly_def by auto
   2.287 -  thus ?thesis
   2.288 -    using True unfolding is_root_def by simp
   2.289 -next
   2.290 -  case False
   2.291 -  interpret UP: domain "poly_ring R"
   2.292 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.293 -
   2.294 -  { fix p q
   2.295 -    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"
   2.296 -    have "is_root p x \<Longrightarrow> is_root q x"
   2.297 -    proof -
   2.298 -      assume is_root: "is_root p x"
   2.299 -      then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
   2.300 -        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
   2.301 -      moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   2.302 -        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
   2.303 -      ultimately have "[ \<one>, \<ominus> x ] pdivides q"
   2.304 -        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
   2.305 -      with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
   2.306 -        using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
   2.307 -              pdivides_imp_is_root[of q x]
   2.308 -        by fastforce
   2.309 -    qed
   2.310 -  }
   2.311 -
   2.312 -  then show ?thesis
   2.313 -    using assms UP.associated_sym[OF assms(3)] by blast
   2.314 -qed
   2.315 -
   2.316 -lemma (in ring) monic_degree_one_root_condition:
   2.317 -  assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
   2.318 -  using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
   2.319 -
   2.320 -lemma (in field) degree_one_root_condition:
   2.321 -  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
   2.322 -  shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
   2.323 -proof -
   2.324 -  interpret UP: domain "poly_ring R"
   2.325 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.326 -
   2.327 -  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
   2.328 -    by simp
   2.329 -  then obtain a b where p: "p = [ a, b ]"
   2.330 -    by (metis length_0_conv length_Cons list.exhaust nat.inject)
   2.331 -  hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
   2.332 -    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.333 -  hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
   2.334 -    using subfield_m_inv[OF carrier_is_subfield, of a] by auto
   2.335 -  hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
   2.336 -    using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.337 -
   2.338 -  have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
   2.339 -  proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
   2.340 -    have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
   2.341 -      using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
   2.342 -    also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
   2.343 -      using UP.m_comm[OF in_carrier, of "[ a ]"] a
   2.344 -      by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
   2.345 -    finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
   2.346 -  next
   2.347 -    from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
   2.348 -      unfolding univ_poly_units[OF carrier_is_subfield] by simp
   2.349 -  qed
   2.350 -
   2.351 -  moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
   2.352 -    and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
   2.353 -    using inv_a a b unfolding p const_term_def by auto
   2.354 -
   2.355 -  ultimately show ?thesis
   2.356 -    using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
   2.357 -          monic_degree_one_root_condition
   2.358 -    by (metis add.inv_closed)
   2.359 -qed
   2.360 -
   2.361 -lemma (in domain) is_root_imp_is_root_poly_mult:
   2.362 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "q \<noteq> []"
   2.363 -  shows "is_root p x \<Longrightarrow> is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
   2.364 -proof -
   2.365 -  interpret UP: domain "poly_ring R"
   2.366 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.367 -
   2.368 -  assume "is_root p x" then have x: "x \<in> carrier R" and eval: "eval p x = \<zero>" and not_zero: "p \<noteq> []"
   2.369 -    unfolding is_root_def by simp+
   2.370 -  hence "p \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
   2.371 -    using assms UP.integral unfolding sym[OF univ_poly_zero[of R "carrier R"]] by blast
   2.372 -  moreover have "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
   2.373 -    using assms eval ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by auto
   2.374 -  ultimately show ?thesis
   2.375 -    using x unfolding is_root_def by simp
   2.376 -qed
   2.377 -
   2.378 -lemma (in domain) is_root_poly_mult_imp_is_root:
   2.379 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
   2.380 -  shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
   2.381 -proof -
   2.382 -  interpret UP: domain "poly_ring R"
   2.383 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.384 -
   2.385 -  assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
   2.386 -  hence "p \<noteq> []" and "q \<noteq> []"
   2.387 -    unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
   2.388 -    using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
   2.389 -  moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
   2.390 -    using is_root unfolding is_root_def by simp+
   2.391 -  hence "eval p x = \<zero> \<or> eval q x = \<zero>"
   2.392 -    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto
   2.393 -  ultimately show "(is_root p x) \<or> (is_root q x)"
   2.394 -    using x unfolding is_root_def by auto
   2.395 -qed
   2.396 -
   2.397 -(*
   2.398 -lemma (in domain)
   2.399 -  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
   2.400 -  shows "pprime K p"
   2.401 -proof (rule pprimeI[OF assms(1-2)])
   2.402 -  from \<open>degree p = 1\<close> show "p \<noteq> []" and "p \<notin> Units (K [X])"
   2.403 -    unfolding univ_poly_units[OF assms(1)] by auto
   2.404 -next
   2.405 -  fix q r
   2.406 -  assume "q \<in> carrier (K[X])" and "r \<in> carrier (K[X])"
   2.407 -    and pdiv: "p pdivides q \<otimes>\<^bsub>K [X]\<^esub> r"
   2.408 -  hence "q \<in> carrier (poly_ring R)" and "r \<in> carrier (poly_ring R)"
   2.409 -    using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
   2.410 -  moreover obtain b where b: "b \<in>"
   2.411 -qed
   2.412 -*)
   2.413 -
   2.414 -lemma (in domain) finite_number_of_roots:
   2.415 -  assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
   2.416 -  using assms
   2.417 -proof (induction "degree p" arbitrary: p)
   2.418 -  case 0 thus ?case
   2.419 -    by (simp add: degree_zero_imp_not_is_root)
   2.420 -next
   2.421 -  case (Suc n) show ?case
   2.422 -  proof (cases "{ x. is_root p x } = {}")
   2.423 -    case True thus ?thesis
   2.424 -      by (simp add: True)
   2.425 -  next
   2.426 -    interpret UP: domain "poly_ring R"
   2.427 -      using univ_poly_is_domain[OF carrier_is_subring] .
   2.428 -
   2.429 -    case False
   2.430 -    then obtain a where is_root: "is_root p a"
   2.431 -      by blast
   2.432 -    hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
   2.433 -      unfolding is_root_def by auto
   2.434 -    hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   2.435 -      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.436 -
   2.437 -    obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
   2.438 -      using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
   2.439 -    with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
   2.440 -      using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
   2.441 -      by metis
   2.442 -    hence "degree q = n"
   2.443 -      using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
   2.444 -            in_carrier q p_not_zero p Suc(2)
   2.445 -      unfolding univ_poly_carrier
   2.446 -      by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
   2.447 -                list.size(3-4) plus_1_eq_Suc univ_poly_mult)
   2.448 -    hence "finite { x. is_root q x }"
   2.449 -      using Suc(1)[OF _ q] by simp
   2.450 -
   2.451 -    moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
   2.452 -      using is_root_poly_mult_imp_is_root[OF in_carrier q]
   2.453 -            monic_degree_one_root_condition[OF a]
   2.454 -      unfolding p by auto
   2.455 -
   2.456 -    ultimately show ?thesis
   2.457 -      using finite_subset by auto
   2.458 -  qed
   2.459 -qed
   2.460 -
   2.461 -lemma (in domain) alg_multE:
   2.462 -  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
   2.463 -  shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
   2.464 -    and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
   2.465 -proof -
   2.466 -  interpret UP: domain "poly_ring R"
   2.467 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.468 -
   2.469 -  let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
   2.470 -
   2.471 -  define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
   2.472 -  have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
   2.473 -    using UP.nat_pow_0 by simp
   2.474 -  hence "0 \<in> S"
   2.475 -    using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
   2.476 -  hence "S \<noteq> {}"
   2.477 -    by auto
   2.478 -
   2.479 -  moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
   2.480 -  proof -
   2.481 -    have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   2.482 -      using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.483 -    hence "?ppow n \<in> carrier (poly_ring R)"
   2.484 -      using assms unfolding univ_poly_zero by auto
   2.485 -    with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
   2.486 -      using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
   2.487 -    with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
   2.488 -      using polynomial_pow_degree by simp
   2.489 -  qed
   2.490 -  hence "finite S"
   2.491 -    using finite_nat_set_iff_bounded_le by blast
   2.492 -
   2.493 -  ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
   2.494 -    using Max_ge[of S] Max_in[of S] by auto
   2.495 -  with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
   2.496 -    using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
   2.497 -    unfolding S_def alg_mult_def by auto
   2.498 -  thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
   2.499 -   and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
   2.500 -    using MaxS unfolding S_def by auto
   2.501 -qed
   2.502 -
   2.503 -lemma (in domain) le_alg_mult_imp_pdivides:
   2.504 -  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
   2.505 -  shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
   2.506 -proof -
   2.507 -  interpret UP: domain "poly_ring R"
   2.508 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.509 -
   2.510 -  assume le_alg_mult: "n \<le> alg_mult p x"
   2.511 -  have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   2.512 -    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.513 -  hence ppow_pdivides:
   2.514 -    "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
   2.515 -     ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
   2.516 -    using polynomial_pow_division[OF _ le_alg_mult] by simp
   2.517 -
   2.518 -  show ?thesis
   2.519 -  proof (cases "p = []")
   2.520 -    case True thus ?thesis
   2.521 -      using in_carrier pdivides_zero[OF carrier_is_subring] by auto
   2.522 -  next
   2.523 -    case False thus ?thesis
   2.524 -      using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
   2.525 -      unfolding pdivides_def by meson
   2.526 -  qed
   2.527 -qed
   2.528 -
   2.529 -lemma (in domain) alg_mult_gt_zero_iff_is_root:
   2.530 -  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
   2.531 -proof -
   2.532 -  interpret UP: domain "poly_ring R"
   2.533 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.534 -  show ?thesis
   2.535 -  proof
   2.536 -    assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
   2.537 -      unfolding is_root_def by auto
   2.538 -    have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
   2.539 -      using x unfolding univ_poly_def by auto
   2.540 -    thus "alg_mult p x > 0"
   2.541 -      using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
   2.542 -  next
   2.543 -    assume gt_zero: "alg_mult p x > 0"
   2.544 -    hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
   2.545 -      unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
   2.546 -    hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   2.547 -      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.548 -    with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
   2.549 -      using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
   2.550 -    thus "is_root p x"
   2.551 -      using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
   2.552 -  qed
   2.553 -qed
   2.554 -
   2.555 -lemma (in domain) alg_mult_in_multiset:
   2.556 -  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p \<in> multiset"
   2.557 -  using assms alg_mult_gt_zero_iff_is_root finite_number_of_roots unfolding multiset_def by auto
   2.558 -
   2.559 -lemma (in domain) alg_mult_eq_count_roots:
   2.560 -  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
   2.561 -  using alg_mult_in_multiset[OF assms] by (simp add: roots_def)
   2.562 -
   2.563 -lemma (in domain) roots_mem_iff_is_root:
   2.564 -  assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
   2.565 -  using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
   2.566 -  unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
   2.567 -
   2.568 -lemma (in domain) degree_zero_imp_empty_roots:
   2.569 -  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
   2.570 -proof -
   2.571 -  have "alg_mult p = (\<lambda>x. 0)"
   2.572 -  proof (cases "p = []")
   2.573 -    case True thus ?thesis
   2.574 -      using assms unfolding alg_mult_def by auto
   2.575 -  next
   2.576 -    case False hence "length p = Suc 0"
   2.577 -      using assms(2) by (simp add: le_Suc_eq)
   2.578 -    then obtain a where "a \<in> carrier R" and "a \<noteq> \<zero>" and p: "p = [ a ]"
   2.579 -      using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def
   2.580 -      by (metis Suc_length_conv hd_in_set length_0_conv list.sel(1) subset_code(1))
   2.581 -    show ?thesis
   2.582 -    proof (rule ccontr)
   2.583 -      assume "alg_mult p \<noteq> (\<lambda>x. 0)"
   2.584 -      then obtain x where "alg_mult p x > 0"
   2.585 -        by auto
   2.586 -      with \<open>p \<noteq> []\<close> have "eval p x = \<zero>"
   2.587 -        using alg_mult_gt_zero_iff_is_root[OF assms(1), of x] unfolding is_root_def by simp
   2.588 -      with \<open>a \<in> carrier R\<close> have "a = \<zero>"
   2.589 -        unfolding p by auto
   2.590 -      with \<open>a \<noteq> \<zero>\<close> show False ..
   2.591 -    qed
   2.592 -  qed
   2.593 -  thus ?thesis
   2.594 -    by (simp add: roots_def zero_multiset.abs_eq)
   2.595 -qed
   2.596 -
   2.597 -lemma (in domain) degree_zero_imp_splitted:
   2.598 -  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
   2.599 -  unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
   2.600 -
   2.601 -lemma (in domain) roots_inclI':
   2.602 -  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"
   2.603 -  shows "roots p \<subseteq># m"
   2.604 -proof (intro mset_subset_eqI)
   2.605 -  fix a show "count (roots p) a \<le> count m a"
   2.606 -    using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
   2.607 -    by (cases "p = []", simp, cases "a \<in> carrier R", auto)
   2.608 -qed
   2.609 -
   2.610 -lemma (in domain) roots_inclI:
   2.611 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
   2.612 -    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"
   2.613 -  shows "roots p \<subseteq># roots q"
   2.614 -  using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
   2.615 -  unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
   2.616 -
   2.617 -lemma (in domain) pdivides_imp_roots_incl:
   2.618 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
   2.619 -  shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
   2.620 -proof (rule roots_inclI[OF assms])
   2.621 -  interpret UP: domain "poly_ring R"
   2.622 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.623 -
   2.624 -  fix a assume "p pdivides q" and a: "a \<in> carrier R"
   2.625 -  hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
   2.626 -    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   2.627 -  with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
   2.628 -    using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
   2.629 -    by (auto simp add: pdivides_def)
   2.630 -qed
   2.631 -
   2.632 -lemma (in domain) associated_polynomials_imp_same_roots:
   2.633 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
   2.634 -  shows "roots p = roots q"
   2.635 -  using assms pdivides_imp_roots_incl zero_pdivides
   2.636 -  unfolding pdivides_def associated_def
   2.637 -  by (metis subset_mset.eq_iff)
   2.638 -
   2.639 -(* MOVE to Polynomial_Divisibility.thy *)
   2.640 -lemma (in comm_monoid_cancel) prime_pow_divides_iff:
   2.641 -  assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
   2.642 -  shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
   2.643 -proof
   2.644 -  assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
   2.645 -    using divides_prod_l[of "p [^] n" b a] assms by simp
   2.646 -next
   2.647 -  assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
   2.648 -  proof (induction n)
   2.649 -    case 0 with \<open>b \<in> carrier G\<close> show ?case
   2.650 -      by (simp add: unit_divides)
   2.651 -  next
   2.652 -    case (Suc n)
   2.653 -    hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
   2.654 -      using assms(1) divides_prod_r by auto
   2.655 -    with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
   2.656 -      where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
   2.657 -        and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
   2.658 -      using assms by blast
   2.659 -    hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
   2.660 -      using assms by (simp add: m_assoc m_lcomm)
   2.661 -    hence "a \<otimes> c = p \<otimes> d"
   2.662 -      using c d assms(1) assms(2) l_cancel by blast
   2.663 -    with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
   2.664 -      by (metis assms(2) c d dividesI' prime_divides)
   2.665 -    with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
   2.666 -      using assms(1) c by simp
   2.667 -  qed
   2.668 -qed
   2.669 -
   2.670 -(* MOVE to Polynomial_Divisibility.thy *)
   2.671 -lemma (in domain) pirreducible_pow_pdivides_iff:
   2.672 -  assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
   2.673 -    and "pirreducible K p" and "\<not> (p pdivides q)"
   2.674 -  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"
   2.675 -proof -
   2.676 -  interpret UP: principal_domain "K[X]"
   2.677 -    using univ_poly_is_principal[OF assms(1)] .
   2.678 -  show ?thesis
   2.679 -  proof (cases "r = []")
   2.680 -    case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
   2.681 -      unfolding  sym[OF univ_poly_zero[of R K]] by auto
   2.682 -    thus ?thesis
   2.683 -      using pdivides_zero[OF subfieldE(1),of K] assms by auto
   2.684 -  next
   2.685 -    case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
   2.686 -      using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
   2.687 -            UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
   2.688 -    from \<open>p \<noteq> []\<close>
   2.689 -    have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
   2.690 -      using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
   2.691 -    have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
   2.692 -      using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
   2.693 -    have prime: "prime (mult_of (K[X])) p"
   2.694 -      using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
   2.695 -      unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
   2.696 -    have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
   2.697 -      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
   2.698 -      using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
   2.699 -      unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
   2.700 -    thus ?thesis
   2.701 -      using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
   2.702 -      unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
   2.703 -      by (metis DiffI UP.m_closed singletonD)
   2.704 -  qed
   2.705 -qed
   2.706 -
   2.707 -(* MOVE to Polynomial_Divisibility.thy *)
   2.708 -lemma (in domain) univ_poly_units':
   2.709 -  assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
   2.710 -  unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
   2.711 -  by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
   2.712 -
   2.713 -(* MOVE to Polynomial_Divisibility.thy *)
   2.714 -lemma (in domain) subring_degree_one_imp_pirreducible:
   2.715 -  assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
   2.716 -  shows "pirreducible K [ a, b ]"
   2.717 -proof (rule pirreducibleI[OF assms(1)])
   2.718 -  have "a \<in> K" and "a \<noteq> \<zero>"
   2.719 -    using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
   2.720 -  thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
   2.721 -    using univ_poly_units_incl[OF assms(1)] assms(2-3)
   2.722 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.723 -next
   2.724 -  interpret UP: domain "K[X]"
   2.725 -    using univ_poly_is_domain[OF assms(1)] .
   2.726 -
   2.727 -  { fix q r
   2.728 -    assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
   2.729 -    hence not_zero: "q \<noteq> []" "r \<noteq> []"
   2.730 -      by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
   2.731 -    have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
   2.732 -      using not_zero poly_mult_degree_eq[OF assms(1)] q r
   2.733 -      by (simp add: univ_poly_carrier univ_poly_mult)
   2.734 -    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> []"
   2.735 -      using not_zero by auto
   2.736 -  } note aux_lemma1 = this
   2.737 -
   2.738 -  { fix q r
   2.739 -    assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
   2.740 -      and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
   2.741 -    hence "length q = Suc (Suc 0)" and "length r = Suc 0"
   2.742 -      by (linarith, metis add.right_neutral add_eq_if length_0_conv)
   2.743 -    from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
   2.744 -      by (metis length_0_conv length_Cons list.exhaust nat.inject)
   2.745 -    from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
   2.746 -      by (metis length_0_conv length_Suc_conv)
   2.747 -    from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
   2.748 -    have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
   2.749 -      using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.750 -    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
   2.751 -      using poly_mult_lead_coeff[OF assms(1), of q r]
   2.752 -      unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
   2.753 -    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>"
   2.754 -      using assms(2) unfolding Units_def by auto
   2.755 -    hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
   2.756 -      using subringE(1)[OF assms(1)] integral_iff by auto
   2.757 -    with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
   2.758 -      using subringE(1,6)[OF assms(1)] inv_a integral
   2.759 -      unfolding sym[OF univ_poly_carrier] polynomial_def
   2.760 -      by (auto, meson subsetD)
   2.761 -    moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
   2.762 -      using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
   2.763 -      unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
   2.764 -    ultimately have "r \<in> Units (K[X])"
   2.765 -      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
   2.766 -  } note aux_lemma2 = this
   2.767 -
   2.768 -  fix q r
   2.769 -  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"
   2.770 -  thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
   2.771 -    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
   2.772 -qed
   2.773 -
   2.774 -(* MOVE to Polynomial_Divisibility.thy *)
   2.775 -lemma (in domain) degree_one_imp_pirreducible:
   2.776 -  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
   2.777 -  shows "pirreducible K p"
   2.778 -proof -
   2.779 -  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
   2.780 -    by simp
   2.781 -  then obtain a b where p: "p = [ a, b ]"
   2.782 -    by (metis length_0_conv length_Suc_conv)
   2.783 -  with \<open>p \<in> carrier (K[X])\<close> show ?thesis
   2.784 -    using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
   2.785 -          subfield.subfield_Units[OF assms(1)]
   2.786 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.787 -qed
   2.788 -
   2.789 -(* MOVE to Polynomial_Divisibility.thy *)
   2.790 -lemma (in ring) degree_oneE[elim]:
   2.791 -  assumes "p \<in> carrier (K[X])" and "degree p = 1"
   2.792 -    and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
   2.793 -  shows P
   2.794 -proof -
   2.795 -  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
   2.796 -    by simp
   2.797 -  then obtain a b where "p = [ a, b ]"
   2.798 -    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
   2.799 -  with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
   2.800 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.801 -  with \<open>p = [ a, b ]\<close> show ?thesis
   2.802 -    using assms(3) by simp
   2.803 -qed
   2.804 -
   2.805 -(* MOVE to Polynomial_Divisibility.thy *)
   2.806 -lemma (in domain) subring_degree_one_associatedI:
   2.807 -  assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
   2.808 -  shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
   2.809 -proof -
   2.810 -  from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
   2.811 -    using subringE(1)[OF assms(1)] assms(2-3) by auto
   2.812 -  hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
   2.813 -    using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
   2.814 -    unfolding univ_poly_mult by fastforce
   2.815 -  moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
   2.816 -    using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
   2.817 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.818 -  moreover have "[ a ] \<in> Units (K[X])"
   2.819 -  proof -
   2.820 -    from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
   2.821 -      using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.822 -    moreover have "a' \<otimes> a = \<one>"
   2.823 -      using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp
   2.824 -    hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
   2.825 -      using assms unfolding univ_poly_mult by auto
   2.826 -    ultimately show ?thesis
   2.827 -      unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
   2.828 -  qed
   2.829 -  ultimately show ?thesis
   2.830 -    using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
   2.831 -qed
   2.832 -
   2.833 -(* MOVE to Polynomial_Divisibility.thy *)
   2.834 -lemma (in domain) degree_one_associatedI:
   2.835 -  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
   2.836 -  shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
   2.837 -proof -
   2.838 -  from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
   2.839 -  obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
   2.840 -    by auto
   2.841 -  thus ?thesis
   2.842 -    using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
   2.843 -          subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
   2.844 -    unfolding const_term_def
   2.845 -    by auto
   2.846 -qed
   2.847 -
   2.848 -lemma (in domain) monic_degree_one_roots:
   2.849 -  assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
   2.850 -proof -
   2.851 -  let ?p = "[ \<one> , \<ominus> a ]"
   2.852 -
   2.853 -  interpret UP: domain "poly_ring R"
   2.854 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.855 -
   2.856 -  from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
   2.857 -    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   2.858 -  show ?thesis
   2.859 -  proof (rule subset_mset.antisym)
   2.860 -    show "{# a #} \<subseteq># roots ?p"
   2.861 -      using roots_mem_iff_is_root[OF in_carrier]
   2.862 -            monic_degree_one_root_condition[OF assms]
   2.863 -      by simp
   2.864 -  next
   2.865 -    show "roots ?p \<subseteq># {# a #}"
   2.866 -    proof (rule mset_subset_eqI, auto)
   2.867 -      fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
   2.868 -        using alg_mult_gt_zero_iff_is_root[OF in_carrier]
   2.869 -              monic_degree_one_root_condition[OF assms]
   2.870 -        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
   2.871 -        by fastforce
   2.872 -    next
   2.873 -      have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
   2.874 -        using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
   2.875 -      hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
   2.876 -        using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
   2.877 -      thus "count (roots ?p) a \<le> Suc 0"
   2.878 -        using polynomial_pow_degree[OF in_carrier]
   2.879 -        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
   2.880 -        by auto
   2.881 -    qed
   2.882 -  qed
   2.883 -qed
   2.884 -
   2.885 -lemma (in domain) degree_one_roots:
   2.886 -  assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
   2.887 -  shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
   2.888 -proof -
   2.889 -  have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
   2.890 -    using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.891 -  thus ?thesis
   2.892 -    using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
   2.893 -          monic_degree_one_roots associated_polynomials_imp_same_roots
   2.894 -    by (metis add.inv_closed local.minus_minus m_closed)
   2.895 -qed
   2.896 -
   2.897 -lemma (in field) degree_one_imp_singleton_roots:
   2.898 -  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
   2.899 -  shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
   2.900 -proof -
   2.901 -  from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
   2.902 -  obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
   2.903 -    by auto
   2.904 -  thus ?thesis
   2.905 -    using degree_one_roots[of a "inv a" b]
   2.906 -    by (auto simp add: const_term_def field_Units)
   2.907 -qed
   2.908 -
   2.909 -lemma (in field) degree_one_imp_splitted:
   2.910 -  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
   2.911 -  using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
   2.912 -
   2.913 -lemma (in field) no_roots_imp_same_roots:
   2.914 -  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
   2.915 -  shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
   2.916 -proof -
   2.917 -  interpret UP: domain "poly_ring R"
   2.918 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.919 -
   2.920 -  assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
   2.921 -  proof (intro subset_mset.antisym)
   2.922 -    have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
   2.923 -      using UP.divides_prod_l assms unfolding pdivides_def by blast
   2.924 -    show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
   2.925 -      using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
   2.926 -            degree_zero_imp_empty_roots[OF assms(3)]
   2.927 -      by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
   2.928 -  next
   2.929 -    show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
   2.930 -    proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
   2.931 -      case True thus ?thesis
   2.932 -        using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
   2.933 -    next
   2.934 -      case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
   2.935 -        by (metis UP.r_null assms(1) univ_poly_zero)
   2.936 -      show ?thesis
   2.937 -      proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
   2.938 -        fix a assume a: "a \<in> carrier R"
   2.939 -        hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
   2.940 -          using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
   2.941 -        moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   2.942 -          using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   2.943 -        hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
   2.944 -          using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
   2.945 -        moreover
   2.946 -        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)"
   2.947 -          using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
   2.948 -        ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
   2.949 -          using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
   2.950 -      qed
   2.951 -    qed
   2.952 -  qed
   2.953 -qed
   2.954 -
   2.955 -lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
   2.956 -  assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
   2.957 -  shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
   2.958 -proof -
   2.959 -  interpret UP: domain "poly_ring R"
   2.960 -    using univ_poly_is_domain[OF carrier_is_subring] .
   2.961 -
   2.962 -  from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   2.963 -    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   2.964 -
   2.965 -  show ?thesis
   2.966 -  proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
   2.967 -    show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
   2.968 -      using in_carrier assms(2) by simp
   2.969 -  next
   2.970 -    fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
   2.971 -    hence not_zero: "p \<noteq> []"
   2.972 -      unfolding univ_poly_def by auto
   2.973 -    from \<open>b \<in> carrier R\<close> have in_carrier':  "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
   2.974 -      unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   2.975 -    show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
   2.976 -    proof (cases "a = b")
   2.977 -      case False
   2.978 -      hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
   2.979 -        using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
   2.980 -      moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
   2.981 -        using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
   2.982 -      ultimately
   2.983 -      have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
   2.984 -        using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
   2.985 -              pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
   2.986 -        by auto
   2.987 -      with \<open>a \<noteq> b\<close> show ?thesis
   2.988 -        using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
   2.989 -    next
   2.990 -      case True
   2.991 -      have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
   2.992 -        using dividesI[OF assms(2)] unfolding pdivides_def by auto
   2.993 -      with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
   2.994 -      have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
   2.995 -        using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
   2.996 -      then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
   2.997 -        using Suc_le_D by blast
   2.998 -      hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
   2.999 -             ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
  2.1000 -        using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
  2.1001 -              in_carrier assms UP.nat_pow_Suc2 by force
  2.1002 -      hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
  2.1003 -        using UP.mult_divides in_carrier assms(2)
  2.1004 -        unfolding univ_poly_zero pdivides_def factor_def
  2.1005 -        by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
  2.1006 -      with \<open>a = b\<close> show ?thesis
  2.1007 -        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
  2.1008 -              alg_multE(2)[OF assms(1) _ not_zero] m
  2.1009 -        by auto
  2.1010 -    qed
  2.1011 -  next
  2.1012 -    fix b
  2.1013 -    have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
  2.1014 -      using assms in_carrier univ_poly_zero[of R] UP.integral by auto
  2.1015 -
  2.1016 -    show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
  2.1017 -    proof (cases "a = b")
  2.1018 -      case True
  2.1019 -      have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
  2.1020 -            ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
  2.1021 -        using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
  2.1022 -        by (auto simp add: pdivides_def)
  2.1023 -      with \<open>a = b\<close> show ?thesis
  2.1024 -        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
  2.1025 -              alg_multE(2)[OF assms(1) _ not_zero]
  2.1026 -        by auto
  2.1027 -    next
  2.1028 -      case False
  2.1029 -      have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
  2.1030 -        using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
  2.1031 -      thus ?thesis
  2.1032 -        using False pdivides_imp_roots_incl assms in_carrier not_zero
  2.1033 -        by (simp add: subseteq_mset_def)
  2.1034 -    qed
  2.1035 -  qed
  2.1036 -qed
  2.1037 -
  2.1038 -lemma (in domain) not_empty_rootsE[elim]:
  2.1039 -  assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
  2.1040 -    and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
  2.1041 -               [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
  2.1042 -  shows P
  2.1043 -proof -
  2.1044 -  from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
  2.1045 -    by blast
  2.1046 -  with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
  2.1047 -    and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
  2.1048 -    using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
  2.1049 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  2.1050 -  with \<open>a \<in># roots p\<close> show ?thesis
  2.1051 -    using assms(3)[of a] by auto
  2.1052 -qed
  2.1053 -
  2.1054 -lemma (in field) associated_polynomials_imp_same_roots:
  2.1055 -  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
  2.1056 -  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots p + roots q"
  2.1057 -proof -
  2.1058 -  interpret UP: domain "poly_ring R"
  2.1059 -    using univ_poly_is_domain[OF carrier_is_subring] .
  2.1060 -  from assms show ?thesis
  2.1061 -  proof (induction "degree p" arbitrary: p rule: less_induct)
  2.1062 -    case less show ?case
  2.1063 -    proof (cases "roots p = {#}")
  2.1064 -      case True thus ?thesis
  2.1065 -        using no_roots_imp_same_roots[of p q] less by simp
  2.1066 -    next
  2.1067 -      case False with \<open>p \<in> carrier (poly_ring R)\<close>
  2.1068 -      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
  2.1069 -          and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  2.1070 -        by blast
  2.1071 -      show ?thesis
  2.1072 -      proof (cases "degree p = 1")
  2.1073 -        case True with \<open>p \<in> carrier (poly_ring R)\<close>
  2.1074 -        obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
  2.1075 -          by auto
  2.1076 -        with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
  2.1077 -          and lead: "lead_coeff p = b" and const: "const_term p = c"
  2.1078 -          using degree_one_imp_singleton_roots[of p] less(2) field_Units
  2.1079 -          unfolding const_term_def by auto
  2.1080 -        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)"
  2.1081 -          using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
  2.1082 -          by (auto simp add: a lead const)
  2.1083 -        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
  2.1084 -          using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
  2.1085 -        thus ?thesis
  2.1086 -          unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
  2.1087 -      next
  2.1088 -        case False
  2.1089 -        from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
  2.1090 -        obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
  2.1091 -          unfolding pdivides_def by auto
  2.1092 -        with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
  2.1093 -          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
  2.1094 -        with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
  2.1095 -          using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
  2.1096 -          unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  2.1097 -        with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
  2.1098 -          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
  2.1099 -        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
  2.1100 -          using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
  2.1101 -                UP.m_assoc[OF in_carrier r less(4)] p by auto
  2.1102 -        also have " ... = add_mset a (roots r + roots q)"
  2.1103 -          using less(1)[OF _ r not_zero less(4-5)] deg by simp
  2.1104 -        also have " ... = (add_mset a (roots r)) + roots q"
  2.1105 -          by simp
  2.1106 -        also have " ... = roots p + roots q"
  2.1107 -          using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp
  2.1108 -        finally show ?thesis .
  2.1109 -      qed
  2.1110 -    qed
  2.1111 -  qed
  2.1112 -qed
  2.1113 -
  2.1114 -lemma (in field) size_roots_le_degree:
  2.1115 -  assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
  2.1116 -  using assms
  2.1117 -proof (induction "degree p" arbitrary: p rule: less_induct)
  2.1118 -  case less show ?case
  2.1119 -  proof (cases "roots p = {#}", simp)
  2.1120 -    interpret UP: domain "poly_ring R"
  2.1121 -      using univ_poly_is_domain[OF carrier_is_subring] .
  2.1122 -
  2.1123 -    case False with \<open>p \<in> carrier (poly_ring R)\<close>
  2.1124 -    obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
  2.1125 -      and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  2.1126 -      by blast
  2.1127 -    then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
  2.1128 -      unfolding pdivides_def by auto
  2.1129 -    with \<open>a \<in># roots p\<close> have "p \<noteq> []"
  2.1130 -      using degree_zero_imp_empty_roots[OF less(2)] by auto
  2.1131 -    hence not_zero: "q \<noteq> []"
  2.1132 -      using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
  2.1133 -    hence "degree p = Suc (degree q)"
  2.1134 -      using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
  2.1135 -      unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  2.1136 -    with \<open>q \<noteq> []\<close> show ?thesis
  2.1137 -      using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
  2.1138 -      by (metis Suc_le_mono lessI size_add_mset)
  2.1139 -  qed
  2.1140 -qed
  2.1141 -
  2.1142 -
  2.1143 -(* MOVE to Polynomial_Divisibility.thy ======== *)
  2.1144 -lemma (in ring) divides_pirreducible_condition:
  2.1145 -  assumes "pirreducible K q" and "p \<in> carrier (K[X])"
  2.1146 -  shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
  2.1147 -  using divides_irreducible_condition[of "K[X]" q p] assms
  2.1148 -  unfolding ring_irreducible_def by auto
  2.1149 -
  2.1150 -lemma (in domain) pirreducible_roots:
  2.1151 -  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
  2.1152 -  shows "roots p = {#}"
  2.1153 -proof (rule ccontr)
  2.1154 -  assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
  2.1155 -  obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
  2.1156 -    and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  2.1157 -    by blast
  2.1158 -  hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
  2.1159 -    using divides_pirreducible_condition[OF assms(2) in_carrier]
  2.1160 -          univ_poly_units_incl[OF carrier_is_subring]
  2.1161 -    unfolding pdivides_def by auto
  2.1162 -  hence "degree p = 1"
  2.1163 -    using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
  2.1164 -  with \<open>degree p \<noteq> 1\<close> show False ..
  2.1165 -qed
  2.1166 -
  2.1167 -lemma (in field) pirreducible_imp_not_splitted:
  2.1168 -  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
  2.1169 -  shows "\<not> splitted p"
  2.1170 -  using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
  2.1171 -  by (simp add: splitted_def)
  2.1172 -
  2.1173 -lemma (in field)
  2.1174 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
  2.1175 -    and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
  2.1176 -  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
  2.1177 -  using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
  2.1178 -  unfolding ring_irreducible_def univ_poly_zero by auto
  2.1179 -
  2.1180 -lemma (in field) trivial_factors_imp_splitted:
  2.1181 -  assumes "p \<in> carrier (poly_ring R)"
  2.1182 -    and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
  2.1183 -  shows "splitted p"
  2.1184 -  using assms
  2.1185 -proof (induction "degree p" arbitrary: p rule: less_induct)
  2.1186 -  interpret UP: principal_domain "poly_ring R"
  2.1187 -    using univ_poly_is_principal[OF carrier_is_subfield] .
  2.1188 -  case less show ?case
  2.1189 -  proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
  2.1190 -    case False show ?thesis
  2.1191 -    proof (cases "roots p = {#}")
  2.1192 -      case True
  2.1193 -      from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
  2.1194 -        using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
  2.1195 -      then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
  2.1196 -        using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
  2.1197 -      with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
  2.1198 -        using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
  2.1199 -              pdivides_imp_roots_incl[OF _ less(2), of q]
  2.1200 -              pirreducible_degree[OF carrier_is_subfield, of q]
  2.1201 -        by force
  2.1202 -      from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
  2.1203 -        by simp
  2.1204 -      thus ?thesis ..
  2.1205 -    next
  2.1206 -      case False with \<open>p \<in> carrier (poly_ring R)\<close>
  2.1207 -      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
  2.1208 -        and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  2.1209 -        by blast
  2.1210 -      then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
  2.1211 -        unfolding pdivides_def by blast
  2.1212 -      with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
  2.1213 -        by auto
  2.1214 -      with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
  2.1215 -        using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
  2.1216 -      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)"
  2.1217 -        using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
  2.1218 -        unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  2.1219 -      moreover have "q pdivides p"
  2.1220 -        using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
  2.1221 -      hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
  2.1222 -        and "r pdivides q" for r
  2.1223 -        using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
  2.1224 -              pirreducible_degree[OF carrier_is_subfield that(1-2)]
  2.1225 -        by (auto simp add: pdivides_def)
  2.1226 -      ultimately have "splitted q"
  2.1227 -        using less(1)[OF _ q] by auto
  2.1228 -      with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
  2.1229 -        using poly_mult_degree_one_monic_imp_same_roots[OF a q]
  2.1230 -        unfolding sym[OF p] splitted_def
  2.1231 -        by simp
  2.1232 -    qed
  2.1233 -  qed
  2.1234 -qed
  2.1235 -
  2.1236 -lemma (in field) pdivides_imp_splitted:
  2.1237 -  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q"
  2.1238 -  shows "p pdivides q \<Longrightarrow> splitted p"
  2.1239 -proof (cases "p = []")
  2.1240 -  case True thus ?thesis
  2.1241 -    using degree_zero_imp_splitted[OF assms(1)] by simp
  2.1242 -next
  2.1243 -  interpret UP: principal_domain "poly_ring R"
  2.1244 -    using univ_poly_is_principal[OF carrier_is_subfield] .
  2.1245 -
  2.1246 -  case False
  2.1247 -  assume "p pdivides q"
  2.1248 -  then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
  2.1249 -    unfolding pdivides_def by auto
  2.1250 -  with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
  2.1251 -    using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
  2.1252 -  hence "degree p + degree b = size (roots p) + size (roots b)"
  2.1253 -    using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
  2.1254 -          poly_mult_degree_eq[OF carrier_is_subring,of p b]
  2.1255 -    unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
  2.1256 -    by auto
  2.1257 -  moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
  2.1258 -    using size_roots_le_degree assms(1) b by auto
  2.1259 -  ultimately show ?thesis
  2.1260 -    unfolding splitted_def by linarith
  2.1261 -qed
  2.1262 -
  2.1263 -lemma (in field) splitted_imp_trivial_factors:
  2.1264 -  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
  2.1265 -  shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
  2.1266 -  using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
  2.1267 -  by auto
  2.1268 -
  2.1269  lemma (in field) exists_root:
  2.1270    assumes "M \<in> extensions" and "\<And>L. \<lbrakk> L \<in> extensions; M \<lesssim> L \<rbrakk> \<Longrightarrow> law_restrict L = law_restrict M"
  2.1271      and "P \<in> carrier (poly_ring R)"
  2.1272 @@ -1664,7 +523,7 @@
  2.1273    qed
  2.1274    then obtain i :: nat where "\<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
  2.1275      by blast
  2.1276 -
  2.1277 +  
  2.1278    then have hyps:
  2.1279      \<comment> \<open>i\<close>   "field M"
  2.1280      \<comment> \<open>ii\<close>  "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> carrier_coeff \<P>"
  2.1281 @@ -1760,7 +619,7 @@
  2.1282    obtain M where "M \<in> extensions" and "\<forall>L \<in> extensions. M \<lesssim> L \<longrightarrow> law_restrict L = law_restrict M"
  2.1283      using exists_maximal_extension iso_incl_hom by blast
  2.1284    thus ?thesis
  2.1285 -    using exists_root[of M] by auto
  2.1286 +    using exists_root[of M] by auto 
  2.1287  qed
  2.1288  
  2.1289  
  2.1290 @@ -1773,9 +632,9 @@
  2.1291  locale algebraically_closed = field L for L (structure) +
  2.1292    assumes roots_over_carrier: "P \<in> carrier (poly_ring L) \<Longrightarrow> splitted P"
  2.1293  
  2.1294 -definition (in field) closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring" ("\<Omega>")
  2.1295 -  where "closure = (SOME L \<comment> \<open>such that\<close>.
  2.1296 -           \<comment> \<open>i\<close>  algebraic_closure L (indexed_const ` (carrier R)) \<and>
  2.1297 +definition (in field) alg_closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
  2.1298 +  where "alg_closure = (SOME L \<comment> \<open>such that\<close>.
  2.1299 +           \<comment> \<open>i\<close>  algebraic_closure L (indexed_const ` (carrier R)) \<and> 
  2.1300             \<comment> \<open>ii\<close> indexed_const \<in> ring_hom R L)"
  2.1301  
  2.1302  lemma algebraic_hom:
  2.1303 @@ -1961,7 +820,7 @@
  2.1304              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>
  2.1305              have "degree R = 1"
  2.1306                using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M]
  2.1307 -                    Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force
  2.1308 +                    Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force  
  2.1309              thus ?thesis
  2.1310                by simp
  2.1311            qed
  2.1312 @@ -1978,11 +837,26 @@
  2.1313      using that by auto
  2.1314  qed
  2.1315  
  2.1316 -lemma (in field) closureE:
  2.1317 -  shows "algebraic_closure \<Omega> (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R \<Omega>"
  2.1318 -  using exists_closure unfolding closure_def
  2.1319 +lemma (in field) alg_closureE:
  2.1320 +  shows "algebraic_closure alg_closure (indexed_const ` (carrier R))"
  2.1321 +    and "indexed_const \<in> ring_hom R alg_closure"
  2.1322 +  using exists_closure unfolding alg_closure_def
  2.1323    by (metis (mono_tags, lifting) someI2)+
  2.1324  
  2.1325 +lemma (in field) algebraically_closedI':
  2.1326 +  assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> splitted p"
  2.1327 +  shows "algebraically_closed R"
  2.1328 +proof
  2.1329 +  fix p assume "p \<in> carrier (poly_ring R)" show "splitted p"
  2.1330 +  proof (cases "degree p \<le> 1")
  2.1331 +    case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
  2.1332 +      using degree_zero_imp_splitted degree_one_imp_splitted by fastforce
  2.1333 +  next
  2.1334 +    case False with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
  2.1335 +      using assms by fastforce
  2.1336 +  qed
  2.1337 +qed
  2.1338 +
  2.1339  lemma (in field) algebraically_closedI:
  2.1340    assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier R. eval p x = \<zero>"
  2.1341    shows "algebraically_closed R"
  2.1342 @@ -2014,13 +888,13 @@
  2.1343        moreover have "roots p = add_mset a (roots q)"
  2.1344          using poly_mult_degree_one_monic_imp_same_roots[OF a(1) q not_zero] p by simp
  2.1345        ultimately show ?thesis
  2.1346 -        unfolding splitted_def deg by simp
  2.1347 +        unfolding splitted_def deg by simp 
  2.1348      qed
  2.1349    qed
  2.1350  qed
  2.1351  
  2.1352  sublocale algebraic_closure \<subseteq> algebraically_closed
  2.1353 -proof (rule algebraically_closedI)
  2.1354 +proof (rule algebraically_closedI')
  2.1355    fix P assume in_carrier: "P \<in> carrier (poly_ring L)" and gt_one: "degree P > 1"
  2.1356    then have gt_zero: "degree P > 0"
  2.1357      by simp
  2.1358 @@ -2074,11 +948,11 @@
  2.1359            univ_poly_subfield_of_consts[OF subfield_axioms] by auto
  2.1360  
  2.1361    moreover from \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "poly_of_const ` K \<subseteq> carrier (A[X])"
  2.1362 -    using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp
  2.1363 +    using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp 
  2.1364  
  2.1365    ultimately
  2.1366    have "subalgebra (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X])) (Rupt A P)"
  2.1367 -    using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp
  2.1368 +    using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp 
  2.1369  
  2.1370    moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carrier (Rupt A P))"
  2.1371    proof (intro Rupt.telescopic_base_dim(1)[where
  2.1372 @@ -2113,7 +987,7 @@
  2.1373  
  2.1374    ultimately
  2.1375    have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X]))"
  2.1376 -    using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp
  2.1377 +    using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp 
  2.1378  
  2.1379    hence "\<not> inj_on (rupture_surj A P) (carrier (K[X]))"
  2.1380      using Hom'.infinite_dimension_hom[OF _ rupture_one_not_zero[OF A P gt_zero] _
  2.1381 @@ -2129,14 +1003,11 @@
  2.1382      unfolding cgenideal_def by blast
  2.1383    with \<open>P \<in> carrier (A[X])\<close> have "P pdivides Q"
  2.1384      using dividesI[of _ "A[X]"] UP_A.m_comm pdivides_iff_shell[OF A] by simp
  2.1385 -  hence "splitted P"
  2.1386 +  thus "splitted P"
  2.1387      using pdivides_imp_splitted[OF in_carrier
  2.1388            carrier_polynomial_shell[OF subfieldE(1)[OF subfield_axioms] Q(1)] Q(2)
  2.1389 -          roots_over_subfield[OF Q(1)]] Q by simp
  2.1390 -  with \<open>degree P > 1\<close> obtain a where "a \<in># roots P"
  2.1391 -    unfolding splitted_def by force
  2.1392 -  thus "\<exists>x\<in>carrier L. eval P x = \<zero>"
  2.1393 -    unfolding roots_mem_iff_is_root[OF in_carrier] is_root_def by blast
  2.1394 +          roots_over_subfield[OF Q(1)]] Q
  2.1395 +    by simp
  2.1396  qed
  2.1397  
  2.1398  end
     3.1 --- a/src/HOL/Algebra/Divisibility.thy	Mon Apr 29 17:11:26 2019 +0100
     3.2 +++ b/src/HOL/Algebra/Divisibility.thy	Tue Apr 30 11:57:45 2019 +0100
     3.3 @@ -780,6 +780,36 @@
     3.4      using A(1) Units_one_closed b'(1) unit_factor by presburger
     3.5  qed
     3.6  
     3.7 +lemma (in comm_monoid_cancel) prime_pow_divides_iff:
     3.8 +  assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
     3.9 +  shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
    3.10 +proof
    3.11 +  assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
    3.12 +    using divides_prod_l[of "p [^] n" b a] assms by simp  
    3.13 +next
    3.14 +  assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
    3.15 +  proof (induction n)
    3.16 +    case 0 with \<open>b \<in> carrier G\<close> show ?case
    3.17 +      by (simp add: unit_divides)
    3.18 +  next
    3.19 +    case (Suc n)
    3.20 +    hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
    3.21 +      using assms(1) divides_prod_r by auto
    3.22 +    with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
    3.23 +      where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
    3.24 +        and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
    3.25 +      using assms by blast
    3.26 +    hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
    3.27 +      using assms by (simp add: m_assoc m_lcomm)
    3.28 +    hence "a \<otimes> c = p \<otimes> d"
    3.29 +      using c d assms(1) assms(2) l_cancel by blast
    3.30 +    with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
    3.31 +      by (metis assms(2) c d dividesI' prime_divides)
    3.32 +    with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
    3.33 +      using assms(1) c by simp
    3.34 +  qed
    3.35 +qed
    3.36 +
    3.37  
    3.38  subsection \<open>Factorization and Factorial Monoids\<close>
    3.39  
     4.1 --- a/src/HOL/Algebra/Finite_Extensions.thy	Mon Apr 29 17:11:26 2019 +0100
     4.2 +++ b/src/HOL/Algebra/Finite_Extensions.thy	Tue Apr 30 11:57:45 2019 +0100
     4.3 @@ -293,8 +293,11 @@
     4.4          using assms(1) lin(2) unfolding polynomial_def by auto
     4.5        hence "eval (normalize (p @ [ k2 ])) x = k1 \<otimes> x \<oplus> k2"
     4.6          using eval_append_aux[of p k2 x] eval_normalize[of "p @ [ k2 ]" x] assms(2) p(3) by auto
     4.7 -      thus ?case
     4.8 -        using normalize_gives_polynomial[of "p @ [ k2 ]"] polynomial_incl[OF p(2)] lin(2)
     4.9 +      moreover have "set (p @ [k2]) \<subseteq> K"
    4.10 +        using polynomial_incl[OF p(2)] \<open>k2 \<in> K\<close> by auto
    4.11 +      then have "local.normalize (p @ [k2]) \<in> carrier (K [X])"
    4.12 +        using normalize_gives_polynomial univ_poly_carrier by blast
    4.13 +      ultimately show ?case
    4.14          unfolding univ_poly_carrier by force
    4.15      qed
    4.16    qed
    4.17 @@ -720,91 +723,4 @@
    4.18    qed
    4.19  qed
    4.20  
    4.21 -
    4.22 -(*
    4.23 -proposition (in domain) finite_extension_is_subfield:
    4.24 -  assumes "subfield K R" "set xs \<subseteq> carrier R"
    4.25 -  shows "subfield (finite_extension K xs) R \<longleftrightarrow> (algebraic_set over K) (set xs)"
    4.26 -proof
    4.27 -  have "(\<And>x. x \<in> set xs \<Longrightarrow> (algebraic over K) x) \<Longrightarrow> subfield (finite_extension K xs) R"
    4.28 -    using simple_extension_is_subfield algebraic_mono assms
    4.29 -    by (induct xs) (auto, metis finite_extension.simps finite_extension_incl subring_props(1))
    4.30 -  thus "(algebraic_set over K) (set xs) \<Longrightarrow> subfield (finite_extension K xs) R"
    4.31 -    unfolding algebraic_set_def over_def by auto
    4.32 -next
    4.33 -  { fix x xs
    4.34 -    assume x: "x \<in> carrier R" and xs: "set xs \<subseteq> carrier R"
    4.35 -      and is_subfield: "subfield (finite_extension K (x # xs)) R"
    4.36 -    hence "(algebraic over K) x" sorry }
    4.37 -
    4.38 -  assume "subfield (finite_extension K xs) R" thus "(algebraic_set over K) (set xs)"
    4.39 -    using assms(2)
    4.40 -  proof (induct xs)
    4.41 -    case Nil thus ?case
    4.42 -      unfolding algebraic_set_def over_def by simp
    4.43 -  next
    4.44 -    case (Cons x xs)
    4.45 -    have "(algebraic over K) x"
    4.46 -      using simple_extension_subfield_imp_algebraic[OF 
    4.47 -            finite_extension_is_subring[of K xs], of x]
    4.48 -
    4.49 -    then show ?case sorry
    4.50 -  qed
    4.51 -qed
    4.52 -*)
    4.53 -
    4.54 -(*
    4.55 -lemma (in ring) transcendental_imp_trivial_ker:
    4.56 -  assumes "x \<in> carrier R"
    4.57 -  shows "(transcendental over K) x \<Longrightarrow> (\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = [])"
    4.58 -proof -
    4.59 -  fix p assume "(transcendental over K) x" "polynomial R p" "eval p x = \<zero>" "set p \<subseteq> K"
    4.60 -  moreover have "eval [] x = \<zero>" and "polynomial R []"
    4.61 -    using assms zero_is_polynomial by auto
    4.62 -  ultimately show "p = []"
    4.63 -    unfolding over_def transcendental_def inj_on_def by auto
    4.64 -qed
    4.65 -
    4.66 -lemma (in domain) trivial_ker_imp_transcendental:
    4.67 -  assumes "subring K R" and "x \<in> carrier R"
    4.68 -  shows "(\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []) \<Longrightarrow> (transcendental over K) x"
    4.69 -proof -
    4.70 -  assume "\<And>p. \<lbrakk> polynomial R p; set p \<subseteq> K \<rbrakk> \<Longrightarrow> eval p x = \<zero> \<Longrightarrow> p = []"
    4.71 -  hence "a_kernel (univ_poly (R \<lparr> carrier := K \<rparr>)) R (\<lambda>p. local.eval p x) = { [] }"
    4.72 -    unfolding a_kernel_def' univ_poly_subring_def'[OF assms(1)] by auto
    4.73 -  moreover have "[] = \<zero>\<^bsub>(univ_poly (R \<lparr> carrier := K \<rparr>))\<^esub>"
    4.74 -    unfolding univ_poly_def by auto
    4.75 -  ultimately have "inj_on (\<lambda>p. local.eval p x) (carrier (univ_poly (R \<lparr> carrier := K \<rparr>)))"
    4.76 -    using ring_hom_ring.trivial_ker_imp_inj[OF eval_ring_hom[OF assms]] by auto
    4.77 -  thus "(transcendental over K) x"
    4.78 -    unfolding over_def transcendental_def univ_poly_subring_def'[OF assms(1)] by simp
    4.79 -qed
    4.80 -
    4.81 -lemma (in ring) non_trivial_ker_imp_algebraic:
    4.82 -  assumes "x \<in> carrier R"
    4.83 -    and "p \<noteq> []" "polynomial R p" "set p \<subseteq> K" "eval p x = \<zero>"
    4.84 -  shows "(algebraic over K) x"
    4.85 -  using transcendental_imp_trivial_ker[OF assms(1) _ assms(3-5)] assms(2)
    4.86 -  unfolding over_def algebraic_def by auto
    4.87 -
    4.88 -lemma (in domain) algebraic_imp_non_trivial_ker:
    4.89 -  assumes "subring K R" "x \<in> carrier R"
    4.90 -  shows "(algebraic over K) x \<Longrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
    4.91 -  using trivial_ker_imp_transcendental[OF assms]
    4.92 -  unfolding over_def algebraic_def by auto
    4.93 -
    4.94 -lemma (in domain) algebraic_iff:
    4.95 -  assumes "subring K R" "x \<in> carrier R"
    4.96 -  shows "(algebraic over K) x \<longleftrightarrow> (\<exists>p \<noteq> []. polynomial R p \<and> set p \<subseteq> K \<and> eval p x = \<zero>)"
    4.97 -  using non_trivial_ker_imp_algebraic[OF assms(2)] algebraic_imp_non_trivial_ker[OF assms] by auto
    4.98 -*)
    4.99 -
   4.100 -
   4.101 -(*
   4.102 -lemma (in field)
   4.103 -  assumes "subfield K R"
   4.104 -  shows "subfield (simple_extension K x) R \<longleftrightarrow> (algebraic over K) x"
   4.105 -  sorry
   4.106 -
   4.107 -*)
   4.108  end
   4.109 \ No newline at end of file
     5.1 --- a/src/HOL/Algebra/Ideal.thy	Mon Apr 29 17:11:26 2019 +0100
     5.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Apr 30 11:57:45 2019 +0100
     5.3 @@ -193,7 +193,7 @@
     5.4  qed
     5.5  
     5.6  
     5.7 -subsection \<open>General Ideal Properies\<close>
     5.8 +subsection \<open>General Ideal Properties\<close>
     5.9  
    5.10  lemma (in ideal) one_imp_carrier:
    5.11    assumes I_one_closed: "\<one> \<in> I"
    5.12 @@ -210,6 +210,30 @@
    5.13    shows "i \<in> carrier R"
    5.14    using iI by (rule a_Hcarr)
    5.15  
    5.16 +lemma (in ring) quotient_eq_iff_same_a_r_cos:
    5.17 +  assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
    5.18 +  shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
    5.19 +proof
    5.20 +  assume "I +> a = I +> b"
    5.21 +  then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
    5.22 +    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
    5.23 +    unfolding a_r_coset_def' by blast
    5.24 +  hence "a \<ominus> b = i"
    5.25 +    using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
    5.26 +  with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
    5.27 +    by simp
    5.28 +next
    5.29 +  assume "a \<ominus> b \<in> I"
    5.30 +  then obtain i where "i \<in> I" and "a = i \<oplus> b"
    5.31 +    using ideal.Icarr[OF assms(1)] assms(2-3)
    5.32 +    by (metis a_minus_def add.inv_solve_right)
    5.33 +  hence "I +> a = (I +> i) +> b"
    5.34 +    using ideal.Icarr[OF assms(1)] assms(3)
    5.35 +    by (simp add: a_coset_add_assoc subsetI)
    5.36 +  with \<open>i \<in> I\<close> show "I +> a = I +> b"
    5.37 +    using a_rcos_zero[OF assms(1)] by simp
    5.38 +qed
    5.39 +
    5.40  
    5.41  subsection \<open>Intersection of Ideals\<close>
    5.42  
     6.1 --- a/src/HOL/Algebra/Polynomial_Divisibility.thy	Mon Apr 29 17:11:26 2019 +0100
     6.2 +++ b/src/HOL/Algebra/Polynomial_Divisibility.thy	Tue Apr 30 11:57:45 2019 +0100
     6.3 @@ -122,6 +122,11 @@
     6.4    using field.univ_poly_carrier_units[OF subfield_iff(2)[OF assms]]
     6.5          univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto
     6.6  
     6.7 +lemma (in domain) univ_poly_units':
     6.8 +  assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
     6.9 +  unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
    6.10 +  by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
    6.11 +
    6.12  corollary (in domain) rupture_one_not_zero:
    6.13    assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p > 0"
    6.14    shows "\<one>\<^bsub>Rupt K p\<^esub> \<noteq> \<zero>\<^bsub>Rupt K p\<^esub>"
    6.15 @@ -759,6 +764,255 @@
    6.16      using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp
    6.17  qed
    6.18  
    6.19 +lemma (in ring) divides_pirreducible_condition:
    6.20 +  assumes "pirreducible K q" and "p \<in> carrier (K[X])"
    6.21 +  shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
    6.22 +  using divides_irreducible_condition[of "K[X]" q p] assms
    6.23 +  unfolding ring_irreducible_def by auto
    6.24 +
    6.25 +subsection \<open>Polynomial Power\<close>
    6.26 +
    6.27 +lemma (in domain) polynomial_pow_not_zero:
    6.28 +  assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
    6.29 +  shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
    6.30 +proof -
    6.31 +  interpret UP: domain "poly_ring R"
    6.32 +    using univ_poly_is_domain[OF carrier_is_subring] .
    6.33 +
    6.34 +  from assms UP.integral show ?thesis
    6.35 +    unfolding sym[OF univ_poly_zero[of R "carrier R"]]
    6.36 +    by (induction n, auto)
    6.37 +qed
    6.38 +
    6.39 +lemma (in domain) subring_polynomial_pow_not_zero:
    6.40 +  assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
    6.41 +  shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
    6.42 +  using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
    6.43 +  unfolding univ_poly_consistent[OF assms(1)] by simp
    6.44 +
    6.45 +lemma (in domain) polynomial_pow_degree:
    6.46 +  assumes "p \<in> carrier (poly_ring R)"
    6.47 +  shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
    6.48 +proof -
    6.49 +  interpret UP: domain "poly_ring R"
    6.50 +    using univ_poly_is_domain[OF carrier_is_subring] .
    6.51 +
    6.52 +  show ?thesis
    6.53 +  proof (induction n)
    6.54 +    case 0 thus ?case
    6.55 +      using UP.nat_pow_0 unfolding univ_poly_one by auto
    6.56 +  next
    6.57 +    let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
    6.58 +    case (Suc n) thus ?case
    6.59 +    proof (cases "p = []")
    6.60 +      case True thus ?thesis
    6.61 +        using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
    6.62 +    next
    6.63 +      case False
    6.64 +      hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
    6.65 +        using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
    6.66 +      thus ?thesis
    6.67 +        using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
    6.68 +        unfolding univ_poly_carrier univ_poly_zero
    6.69 +        by (auto simp add: add.commute univ_poly_mult)
    6.70 +    qed
    6.71 +  qed
    6.72 +qed
    6.73 +
    6.74 +lemma (in domain) subring_polynomial_pow_degree:
    6.75 +  assumes "subring K R" and "p \<in> carrier (K[X])"
    6.76 +  shows "degree (p [^]\<^bsub>K[X]\<^esub> n) = n * degree p"
    6.77 +  using domain.polynomial_pow_degree[OF subring_is_domain, of K p n] assms
    6.78 +  unfolding univ_poly_consistent[OF assms(1)] by simp
    6.79 +
    6.80 +lemma (in domain) polynomial_pow_division:
    6.81 +  assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
    6.82 +  shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
    6.83 +proof -
    6.84 +  interpret UP: domain "poly_ring R"
    6.85 +    using univ_poly_is_domain[OF carrier_is_subring] .
    6.86 +
    6.87 +  let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
    6.88 +
    6.89 +  have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
    6.90 +    using assms(1) by (simp add: UP.nat_pow_mult)
    6.91 +  thus ?thesis
    6.92 +    using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
    6.93 +    unfolding pdivides_def by auto
    6.94 +qed
    6.95 +
    6.96 +lemma (in domain) subring_polynomial_pow_division:
    6.97 +  assumes "subring K R" and "p \<in> carrier (K[X])" and "(n::nat) \<le> m"
    6.98 +  shows "(p [^]\<^bsub>K[X]\<^esub> n) divides\<^bsub>K[X]\<^esub> (p [^]\<^bsub>K[X]\<^esub> m)"
    6.99 +  using domain.polynomial_pow_division[OF subring_is_domain, of K p n m] assms
   6.100 +  unfolding univ_poly_consistent[OF assms(1)] pdivides_def by simp
   6.101 +
   6.102 +lemma (in domain) pirreducible_pow_pdivides_iff:
   6.103 +  assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
   6.104 +    and "pirreducible K p" and "\<not> (p pdivides q)"
   6.105 +  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"
   6.106 +proof -
   6.107 +  interpret UP: principal_domain "K[X]"
   6.108 +    using univ_poly_is_principal[OF assms(1)] .
   6.109 +  show ?thesis
   6.110 +  proof (cases "r = []")
   6.111 +    case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
   6.112 +      unfolding  sym[OF univ_poly_zero[of R K]] by auto
   6.113 +    thus ?thesis
   6.114 +      using pdivides_zero[OF subfieldE(1),of K] assms by auto
   6.115 +  next
   6.116 +    case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
   6.117 +      using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
   6.118 +            UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
   6.119 +    from \<open>p \<noteq> []\<close>
   6.120 +    have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
   6.121 +      using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
   6.122 +    have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
   6.123 +      using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
   6.124 +    have prime: "prime (mult_of (K[X])) p"
   6.125 +      using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
   6.126 +      unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
   6.127 +    have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
   6.128 +      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
   6.129 +      using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
   6.130 +      unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
   6.131 +    thus ?thesis
   6.132 +      using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
   6.133 +      unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
   6.134 +      by (metis DiffI UP.m_closed singletonD)
   6.135 +  qed
   6.136 +qed
   6.137 +
   6.138 +lemma (in domain) subring_degree_one_imp_pirreducible:
   6.139 +  assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
   6.140 +  shows "pirreducible K [ a, b ]"
   6.141 +proof (rule pirreducibleI[OF assms(1)])
   6.142 +  have "a \<in> K" and "a \<noteq> \<zero>"
   6.143 +    using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
   6.144 +  thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
   6.145 +    using univ_poly_units_incl[OF assms(1)] assms(2-3)
   6.146 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.147 +next
   6.148 +  interpret UP: domain "K[X]"
   6.149 +    using univ_poly_is_domain[OF assms(1)] .
   6.150 +
   6.151 +  { fix q r
   6.152 +    assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
   6.153 +    hence not_zero: "q \<noteq> []" "r \<noteq> []"
   6.154 +      by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
   6.155 +    have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
   6.156 +      using not_zero poly_mult_degree_eq[OF assms(1)] q r
   6.157 +      by (simp add: univ_poly_carrier univ_poly_mult)
   6.158 +    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> []"
   6.159 +      using not_zero by auto
   6.160 +  } note aux_lemma1 = this
   6.161 +
   6.162 +  { fix q r
   6.163 +    assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
   6.164 +      and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
   6.165 +    hence "length q = Suc (Suc 0)" and "length r = Suc 0"
   6.166 +      by (linarith, metis add.right_neutral add_eq_if length_0_conv)
   6.167 +    from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
   6.168 +      by (metis length_0_conv length_Cons list.exhaust nat.inject)
   6.169 +    from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
   6.170 +      by (metis length_0_conv length_Suc_conv)
   6.171 +    from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
   6.172 +    have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
   6.173 +      using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.174 +    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
   6.175 +      using poly_mult_lead_coeff[OF assms(1), of q r]
   6.176 +      unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
   6.177 +    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>"
   6.178 +      using assms(2) unfolding Units_def by auto
   6.179 +    hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
   6.180 +      using subringE(1)[OF assms(1)] integral_iff by auto
   6.181 +    with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
   6.182 +      using subringE(1,6)[OF assms(1)] inv_a integral
   6.183 +      unfolding sym[OF univ_poly_carrier] polynomial_def
   6.184 +      by (auto, meson subsetD)
   6.185 +    moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
   6.186 +      using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
   6.187 +      unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
   6.188 +    ultimately have "r \<in> Units (K[X])"
   6.189 +      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
   6.190 +  } note aux_lemma2 = this
   6.191 +
   6.192 +  fix q r
   6.193 +  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"
   6.194 +  thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
   6.195 +    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
   6.196 +qed
   6.197 +
   6.198 +lemma (in domain) degree_one_imp_pirreducible:
   6.199 +  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
   6.200 +  shows "pirreducible K p"
   6.201 +proof -
   6.202 +  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
   6.203 +    by simp
   6.204 +  then obtain a b where p: "p = [ a, b ]"
   6.205 +    by (metis length_0_conv length_Suc_conv)
   6.206 +  with \<open>p \<in> carrier (K[X])\<close> show ?thesis
   6.207 +    using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
   6.208 +          subfield.subfield_Units[OF assms(1)]
   6.209 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.210 +qed
   6.211 +
   6.212 +lemma (in ring) degree_oneE[elim]:
   6.213 +  assumes "p \<in> carrier (K[X])" and "degree p = 1"
   6.214 +    and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
   6.215 +  shows P
   6.216 +proof -
   6.217 +  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
   6.218 +    by simp
   6.219 +  then obtain a b where "p = [ a, b ]"
   6.220 +    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
   6.221 +  with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
   6.222 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.223 +  with \<open>p = [ a, b ]\<close> show ?thesis
   6.224 +    using assms(3) by simp
   6.225 +qed
   6.226 +
   6.227 +lemma (in domain) subring_degree_one_associatedI:
   6.228 +  assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
   6.229 +  shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
   6.230 +proof -
   6.231 +  from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
   6.232 +    using subringE(1)[OF assms(1)] assms(2-3) by auto
   6.233 +  hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
   6.234 +    using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
   6.235 +    unfolding univ_poly_mult by fastforce
   6.236 +  moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
   6.237 +    using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
   6.238 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.239 +  moreover have "[ a ] \<in> Units (K[X])"
   6.240 +  proof -
   6.241 +    from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
   6.242 +      using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.243 +    moreover have "a' \<otimes> a = \<one>"
   6.244 +      using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp 
   6.245 +    hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
   6.246 +      using assms unfolding univ_poly_mult by auto
   6.247 +    ultimately show ?thesis
   6.248 +      unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
   6.249 +  qed
   6.250 +  ultimately show ?thesis
   6.251 +    using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
   6.252 +qed
   6.253 +
   6.254 +lemma (in domain) degree_one_associatedI:
   6.255 +  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
   6.256 +  shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
   6.257 +proof -
   6.258 +  from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
   6.259 +  obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
   6.260 +    by auto
   6.261 +  thus ?thesis
   6.262 +    using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
   6.263 +          subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
   6.264 +    unfolding const_term_def
   6.265 +    by auto
   6.266 +qed
   6.267 +
   6.268  subsection \<open>Ideals\<close>
   6.269  
   6.270  lemma (in domain) exists_unique_gen:
   6.271 @@ -882,6 +1136,26 @@
   6.272  
   6.273  subsection \<open>Roots and Multiplicity\<close>
   6.274  
   6.275 +definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
   6.276 +  where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
   6.277 +
   6.278 +definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
   6.279 +  where "alg_mult p x =
   6.280 +           (if p = [] then 0 else
   6.281 +             (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
   6.282 +
   6.283 +definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
   6.284 +  where "roots p = Abs_multiset (alg_mult p)"
   6.285 +
   6.286 +definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
   6.287 +  where "roots_on K p = roots p \<inter># mset_set K"
   6.288 +
   6.289 +definition (in ring) splitted :: "'a list \<Rightarrow> bool"
   6.290 +  where "splitted p \<longleftrightarrow> size (roots p) = degree p"
   6.291 +
   6.292 +definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
   6.293 +  where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
   6.294 +
   6.295  lemma (in domain) pdivides_imp_root_sharing:
   6.296    assumes "p \<in> carrier (poly_ring R)" "p pdivides q" and "a \<in> carrier R"
   6.297    shows "eval p a = \<zero> \<Longrightarrow> eval q a = \<zero>"
   6.298 @@ -922,6 +1196,782 @@
   6.299    show "inv (lead_coeff p) \<otimes> (const_term p) \<in> K"
   6.300      using p subringE(6)[OF subfieldE(1)[OF assms(1)]] unfolding ct by auto
   6.301  qed
   6.302 +lemma (in domain) is_root_imp_pdivides:
   6.303 +  assumes "p \<in> carrier (poly_ring R)"
   6.304 +  shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
   6.305 +proof -
   6.306 +  let ?b = "[ \<one> , \<ominus> x ]"
   6.307 +
   6.308 +  interpret UP: domain "poly_ring R"
   6.309 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.310 +
   6.311 +  assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
   6.312 +    unfolding is_root_def by auto
   6.313 +  hence b: "?b \<in> carrier (poly_ring R)"
   6.314 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.315 +  then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
   6.316 +    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"
   6.317 +    using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
   6.318 +
   6.319 +  show ?thesis
   6.320 +  proof (cases "r = []")
   6.321 +    case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
   6.322 +      unfolding univ_poly_zero[of R "carrier R"] .
   6.323 +    thus ?thesis
   6.324 +      using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
   6.325 +  next
   6.326 +    case False then have "length r = Suc 0"
   6.327 +      using long_divides(2) le_SucE by fastforce
   6.328 +    then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
   6.329 +      using r unfolding sym[OF univ_poly_carrier] polynomial_def
   6.330 +      by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
   6.331 +
   6.332 +    have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
   6.333 +      using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
   6.334 +    also have " ... = eval r x"
   6.335 +      using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
   6.336 +    finally have "a = \<zero>"
   6.337 +      using a unfolding \<open>r = [ a ]\<close> is_root by simp
   6.338 +    with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
   6.339 +  qed
   6.340 +qed
   6.341 +
   6.342 +lemma (in domain) pdivides_imp_is_root:
   6.343 +  assumes "p \<noteq> []" and "x \<in> carrier R"
   6.344 +  shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
   6.345 +proof -
   6.346 +  assume "[ \<one>, \<ominus> x ] pdivides p"
   6.347 +  then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
   6.348 +    unfolding pdivides_def by auto
   6.349 +  moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   6.350 +    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   6.351 +  ultimately have "eval p x = \<zero>"
   6.352 +    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
   6.353 +  with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
   6.354 +    unfolding is_root_def by simp 
   6.355 +qed
   6.356 +
   6.357 +lemma (in domain) associated_polynomials_imp_same_is_root:
   6.358 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
   6.359 +  shows "is_root p x \<longleftrightarrow> is_root q x"
   6.360 +proof (cases "p = []")
   6.361 +  case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
   6.362 +    unfolding associated_def True factor_def univ_poly_def by auto
   6.363 +  thus ?thesis
   6.364 +    using True unfolding is_root_def by simp 
   6.365 +next
   6.366 +  case False
   6.367 +  interpret UP: domain "poly_ring R"
   6.368 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.369 +
   6.370 +  { fix p q
   6.371 +    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"
   6.372 +    have "is_root p x \<Longrightarrow> is_root q x"
   6.373 +    proof -
   6.374 +      assume is_root: "is_root p x"
   6.375 +      then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
   6.376 +        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
   6.377 +      moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   6.378 +        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
   6.379 +      ultimately have "[ \<one>, \<ominus> x ] pdivides q"
   6.380 +        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
   6.381 +      with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
   6.382 +        using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
   6.383 +              pdivides_imp_is_root[of q x]
   6.384 +        by fastforce  
   6.385 +    qed
   6.386 +  }
   6.387 +
   6.388 +  then show ?thesis
   6.389 +    using assms UP.associated_sym[OF assms(3)] by blast 
   6.390 +qed
   6.391 +
   6.392 +lemma (in ring) monic_degree_one_root_condition:
   6.393 +  assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
   6.394 +  using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
   6.395 +
   6.396 +lemma (in field) degree_one_root_condition:
   6.397 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
   6.398 +  shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
   6.399 +proof -
   6.400 +  interpret UP: domain "poly_ring R"
   6.401 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.402 +
   6.403 +  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
   6.404 +    by simp
   6.405 +  then obtain a b where p: "p = [ a, b ]"
   6.406 +    by (metis length_0_conv length_Cons list.exhaust nat.inject)
   6.407 +  hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
   6.408 +    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.409 +  hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
   6.410 +    using subfield_m_inv[OF carrier_is_subfield, of a] by auto
   6.411 +  hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
   6.412 +    using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.413 +
   6.414 +  have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
   6.415 +  proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
   6.416 +    have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
   6.417 +      using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
   6.418 +    also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
   6.419 +      using UP.m_comm[OF in_carrier, of "[ a ]"] a
   6.420 +      by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
   6.421 +    finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
   6.422 +  next
   6.423 +    from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
   6.424 +      unfolding univ_poly_units[OF carrier_is_subfield] by simp
   6.425 +  qed
   6.426 +
   6.427 +  moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
   6.428 +    and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
   6.429 +    using inv_a a b unfolding p const_term_def by auto
   6.430 +
   6.431 +  ultimately show ?thesis
   6.432 +    using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
   6.433 +          monic_degree_one_root_condition
   6.434 +    by (metis add.inv_closed)
   6.435 +qed
   6.436 +
   6.437 +lemma (in domain) is_root_poly_mult_imp_is_root:
   6.438 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
   6.439 +  shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
   6.440 +proof -
   6.441 +  interpret UP: domain "poly_ring R"
   6.442 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.443 +
   6.444 +  assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
   6.445 +  hence "p \<noteq> []" and "q \<noteq> []"
   6.446 +    unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
   6.447 +    using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
   6.448 +  moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
   6.449 +    using is_root unfolding is_root_def by simp+
   6.450 +  hence "eval p x = \<zero> \<or> eval q x = \<zero>"
   6.451 +    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto 
   6.452 +  ultimately show "(is_root p x) \<or> (is_root q x)"
   6.453 +    using x unfolding is_root_def by auto
   6.454 +qed
   6.455 +
   6.456 +lemma (in domain) degree_zero_imp_not_is_root:
   6.457 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
   6.458 +proof (cases "p = []", simp add: is_root_def)
   6.459 +  case False with \<open>degree p = 0\<close> have "length p = Suc 0"
   6.460 +    using le_SucE by fastforce 
   6.461 +  then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
   6.462 +    using assms unfolding sym[OF univ_poly_carrier] polynomial_def
   6.463 +    by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
   6.464 +  thus ?thesis
   6.465 +    unfolding is_root_def by auto 
   6.466 +qed
   6.467 +
   6.468 +lemma (in domain) finite_number_of_roots:
   6.469 +  assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
   6.470 +  using assms
   6.471 +proof (induction "degree p" arbitrary: p)
   6.472 +  case 0 thus ?case
   6.473 +    by (simp add: degree_zero_imp_not_is_root)
   6.474 +next
   6.475 +  case (Suc n) show ?case
   6.476 +  proof (cases "{ x. is_root p x } = {}")
   6.477 +    case True thus ?thesis
   6.478 +      by (simp add: True) 
   6.479 +  next
   6.480 +    interpret UP: domain "poly_ring R"
   6.481 +      using univ_poly_is_domain[OF carrier_is_subring] .
   6.482 +
   6.483 +    case False
   6.484 +    then obtain a where is_root: "is_root p a"
   6.485 +      by blast
   6.486 +    hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
   6.487 +      unfolding is_root_def by auto
   6.488 +    hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   6.489 +      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.490 +
   6.491 +    obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
   6.492 +      using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
   6.493 +    with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
   6.494 +      using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
   6.495 +      by metis
   6.496 +    hence "degree q = n"
   6.497 +      using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
   6.498 +            in_carrier q p_not_zero p Suc(2)
   6.499 +      unfolding univ_poly_carrier
   6.500 +      by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
   6.501 +                list.size(3-4) plus_1_eq_Suc univ_poly_mult)
   6.502 +    hence "finite { x. is_root q x }"
   6.503 +      using Suc(1)[OF _ q] by simp
   6.504 +
   6.505 +    moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
   6.506 +      using is_root_poly_mult_imp_is_root[OF in_carrier q]
   6.507 +            monic_degree_one_root_condition[OF a]
   6.508 +      unfolding p by auto
   6.509 +
   6.510 +    ultimately show ?thesis
   6.511 +      using finite_subset by auto
   6.512 +  qed
   6.513 +qed
   6.514 +
   6.515 +lemma (in domain) alg_multE:
   6.516 +  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
   6.517 +  shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
   6.518 +    and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
   6.519 +proof -
   6.520 +  interpret UP: domain "poly_ring R"
   6.521 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.522 +
   6.523 +  let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
   6.524 +
   6.525 +  define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
   6.526 +  have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
   6.527 +    using UP.nat_pow_0 by simp
   6.528 +  hence "0 \<in> S"
   6.529 +    using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
   6.530 +  hence "S \<noteq> {}"
   6.531 +    by auto
   6.532 +
   6.533 +  moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
   6.534 +  proof -
   6.535 +    have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   6.536 +      using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.537 +    hence "?ppow n \<in> carrier (poly_ring R)"
   6.538 +      using assms unfolding univ_poly_zero by auto
   6.539 +    with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
   6.540 +      using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
   6.541 +    with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
   6.542 +      using polynomial_pow_degree by simp
   6.543 +  qed
   6.544 +  hence "finite S"
   6.545 +    using finite_nat_set_iff_bounded_le by blast
   6.546 +
   6.547 +  ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
   6.548 +    using Max_ge[of S] Max_in[of S] by auto
   6.549 +  with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
   6.550 +    using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
   6.551 +    unfolding S_def alg_mult_def by auto
   6.552 +  thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
   6.553 +   and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
   6.554 +    using MaxS unfolding S_def by auto
   6.555 +qed
   6.556 +
   6.557 +lemma (in domain) le_alg_mult_imp_pdivides:
   6.558 +  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
   6.559 +  shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
   6.560 +proof -
   6.561 +  interpret UP: domain "poly_ring R"
   6.562 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.563 +
   6.564 +  assume le_alg_mult: "n \<le> alg_mult p x"
   6.565 +  have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   6.566 +    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.567 +  hence ppow_pdivides:
   6.568 +    "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
   6.569 +     ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
   6.570 +    using polynomial_pow_division[OF _ le_alg_mult] by simp
   6.571 +
   6.572 +  show ?thesis
   6.573 +  proof (cases "p = []")
   6.574 +    case True thus ?thesis
   6.575 +      using in_carrier pdivides_zero[OF carrier_is_subring] by auto
   6.576 +  next
   6.577 +    case False thus ?thesis
   6.578 +      using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
   6.579 +      unfolding pdivides_def by meson
   6.580 +  qed
   6.581 +qed
   6.582 +
   6.583 +lemma (in domain) alg_mult_gt_zero_iff_is_root:
   6.584 +  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
   6.585 +proof -
   6.586 +  interpret UP: domain "poly_ring R"
   6.587 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.588 +  show ?thesis
   6.589 +  proof
   6.590 +    assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
   6.591 +      unfolding is_root_def by auto
   6.592 +    have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
   6.593 +      using x unfolding univ_poly_def by auto
   6.594 +    thus "alg_mult p x > 0"
   6.595 +      using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
   6.596 +  next
   6.597 +    assume gt_zero: "alg_mult p x > 0"
   6.598 +    hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
   6.599 +      unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
   6.600 +    hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   6.601 +      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.602 +    with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
   6.603 +      using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
   6.604 +    thus "is_root p x"
   6.605 +      using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
   6.606 +  qed
   6.607 +qed
   6.608 +
   6.609 +lemma (in domain) alg_mult_eq_count_roots:
   6.610 +  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
   6.611 +  using finite_number_of_roots[OF assms]
   6.612 +  unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
   6.613 +  by (simp add: multiset_def roots_def) 
   6.614 +
   6.615 +lemma (in domain) roots_mem_iff_is_root:
   6.616 +  assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
   6.617 +  using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
   6.618 +  unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
   6.619 +
   6.620 +lemma (in domain) degree_zero_imp_empty_roots:
   6.621 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
   6.622 +  using degree_zero_imp_not_is_root[of p] roots_mem_iff_is_root[of p] assms by auto
   6.623 +
   6.624 +lemma (in domain) degree_zero_imp_splitted:
   6.625 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
   6.626 +  unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
   6.627 +
   6.628 +lemma (in domain) roots_inclI':
   6.629 +  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" 
   6.630 +  shows "roots p \<subseteq># m"
   6.631 +proof (intro mset_subset_eqI)
   6.632 +  fix a show "count (roots p) a \<le> count m a"
   6.633 +    using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
   6.634 +    by (cases "p = []", simp, cases "a \<in> carrier R", auto)
   6.635 +qed
   6.636 +
   6.637 +lemma (in domain) roots_inclI:
   6.638 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
   6.639 +    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"
   6.640 +  shows "roots p \<subseteq># roots q"
   6.641 +  using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
   6.642 +  unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
   6.643 +
   6.644 +lemma (in domain) pdivides_imp_roots_incl:
   6.645 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
   6.646 +  shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
   6.647 +proof (rule roots_inclI[OF assms])
   6.648 +  interpret UP: domain "poly_ring R"
   6.649 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.650 +
   6.651 +  fix a assume "p pdivides q" and a: "a \<in> carrier R"
   6.652 +  hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
   6.653 +    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   6.654 +  with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
   6.655 +    using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
   6.656 +    by (auto simp add: pdivides_def)
   6.657 +qed
   6.658 +
   6.659 +lemma (in domain) associated_polynomials_imp_same_roots:
   6.660 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
   6.661 +  shows "roots p = roots q"
   6.662 +  using assms pdivides_imp_roots_incl zero_pdivides
   6.663 +  unfolding pdivides_def associated_def 
   6.664 +  by (metis subset_mset.eq_iff)
   6.665 +
   6.666 +lemma (in domain) monic_degree_one_roots:
   6.667 +  assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
   6.668 +proof -
   6.669 +  let ?p = "[ \<one> , \<ominus> a ]"
   6.670 +
   6.671 +  interpret UP: domain "poly_ring R"
   6.672 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.673 +
   6.674 +  from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
   6.675 +    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   6.676 +  show ?thesis
   6.677 +  proof (rule subset_mset.antisym)
   6.678 +    show "{# a #} \<subseteq># roots ?p"
   6.679 +      using roots_mem_iff_is_root[OF in_carrier]
   6.680 +            monic_degree_one_root_condition[OF assms]
   6.681 +      by simp
   6.682 +  next
   6.683 +    show "roots ?p \<subseteq># {# a #}"
   6.684 +    proof (rule mset_subset_eqI, auto)
   6.685 +      fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
   6.686 +        using alg_mult_gt_zero_iff_is_root[OF in_carrier]
   6.687 +              monic_degree_one_root_condition[OF assms]
   6.688 +        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
   6.689 +        by fastforce
   6.690 +    next
   6.691 +      have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
   6.692 +        using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
   6.693 +      hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
   6.694 +        using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
   6.695 +      thus "count (roots ?p) a \<le> Suc 0"
   6.696 +        using polynomial_pow_degree[OF in_carrier]
   6.697 +        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
   6.698 +        by auto
   6.699 +    qed
   6.700 +  qed
   6.701 +qed
   6.702 +
   6.703 +lemma (in domain) degree_one_roots:
   6.704 +  assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
   6.705 +  shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
   6.706 +proof -
   6.707 +  have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
   6.708 +    using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.709 +  thus ?thesis
   6.710 +    using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
   6.711 +          monic_degree_one_roots associated_polynomials_imp_same_roots
   6.712 +    by (metis add.inv_closed local.minus_minus m_closed)
   6.713 +qed
   6.714 +
   6.715 +lemma (in field) degree_one_imp_singleton_roots:
   6.716 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
   6.717 +  shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
   6.718 +proof -
   6.719 +  from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
   6.720 +  obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
   6.721 +    by auto
   6.722 +  thus ?thesis
   6.723 +    using degree_one_roots[of a "inv a" b]
   6.724 +    by (auto simp add: const_term_def field_Units)
   6.725 +qed
   6.726 +
   6.727 +lemma (in field) degree_one_imp_splitted:
   6.728 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
   6.729 +  using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
   6.730 +
   6.731 +lemma (in field) no_roots_imp_same_roots:
   6.732 +  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
   6.733 +  shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
   6.734 +proof -
   6.735 +  interpret UP: domain "poly_ring R"
   6.736 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.737 +
   6.738 +  assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
   6.739 +  proof (intro subset_mset.antisym)
   6.740 +    have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
   6.741 +      using UP.divides_prod_l assms unfolding pdivides_def by blast
   6.742 +    show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
   6.743 +      using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
   6.744 +            degree_zero_imp_empty_roots[OF assms(3)]
   6.745 +      by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
   6.746 +  next
   6.747 +    show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
   6.748 +    proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
   6.749 +      case True thus ?thesis
   6.750 +        using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
   6.751 +    next
   6.752 +      case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
   6.753 +        by (metis UP.r_null assms(1) univ_poly_zero)
   6.754 +      show ?thesis
   6.755 +      proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
   6.756 +        fix a assume a: "a \<in> carrier R"
   6.757 +        hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
   6.758 +          using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
   6.759 +        moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   6.760 +          using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.761 +        hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
   6.762 +          using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
   6.763 +        moreover
   6.764 +        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)"
   6.765 +          using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
   6.766 +        ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
   6.767 +          using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
   6.768 +      qed
   6.769 +    qed
   6.770 +  qed
   6.771 +qed
   6.772 +
   6.773 +lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
   6.774 +  assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
   6.775 +  shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
   6.776 +proof -
   6.777 +  interpret UP: domain "poly_ring R"
   6.778 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.779 +  
   6.780 +  from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   6.781 +    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   6.782 +
   6.783 +  show ?thesis
   6.784 +  proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
   6.785 +    show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
   6.786 +      using in_carrier assms(2) by simp
   6.787 +  next
   6.788 +    fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
   6.789 +    hence not_zero: "p \<noteq> []"
   6.790 +      unfolding univ_poly_def by auto
   6.791 +    from \<open>b \<in> carrier R\<close> have in_carrier':  "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
   6.792 +      unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   6.793 +    show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
   6.794 +    proof (cases "a = b")
   6.795 +      case False
   6.796 +      hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
   6.797 +        using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
   6.798 +      moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
   6.799 +        using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
   6.800 +      ultimately
   6.801 +      have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
   6.802 +        using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
   6.803 +              pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
   6.804 +        by auto
   6.805 +      with \<open>a \<noteq> b\<close> show ?thesis
   6.806 +        using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
   6.807 +    next
   6.808 +      case True
   6.809 +      have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
   6.810 +        using dividesI[OF assms(2)] unfolding pdivides_def by auto
   6.811 +      with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
   6.812 +      have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
   6.813 +        using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
   6.814 +      then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
   6.815 +        using Suc_le_D by blast
   6.816 +      hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
   6.817 +             ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
   6.818 +        using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
   6.819 +              in_carrier assms UP.nat_pow_Suc2 by force
   6.820 +      hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
   6.821 +        using UP.mult_divides in_carrier assms(2)
   6.822 +        unfolding univ_poly_zero pdivides_def factor_def
   6.823 +        by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
   6.824 +      with \<open>a = b\<close> show ?thesis
   6.825 +        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2 
   6.826 +              alg_multE(2)[OF assms(1) _ not_zero] m
   6.827 +        by auto
   6.828 +    qed
   6.829 +  next
   6.830 +    fix b
   6.831 +    have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
   6.832 +      using assms in_carrier univ_poly_zero[of R] UP.integral by auto
   6.833 +
   6.834 +    show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
   6.835 +    proof (cases "a = b")
   6.836 +      case True
   6.837 +      have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
   6.838 +            ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
   6.839 +        using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
   6.840 +        by (auto simp add: pdivides_def)
   6.841 +      with \<open>a = b\<close> show ?thesis
   6.842 +        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2 
   6.843 +              alg_multE(2)[OF assms(1) _ not_zero]
   6.844 +        by auto
   6.845 +    next
   6.846 +      case False
   6.847 +      have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
   6.848 +        using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
   6.849 +      thus ?thesis
   6.850 +        using False pdivides_imp_roots_incl assms in_carrier not_zero
   6.851 +        by (simp add: subseteq_mset_def)
   6.852 +    qed
   6.853 +  qed
   6.854 +qed
   6.855 +
   6.856 +lemma (in domain) not_empty_rootsE[elim]:
   6.857 +  assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
   6.858 +    and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
   6.859 +               [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
   6.860 +  shows P
   6.861 +proof -
   6.862 +  from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
   6.863 +    by blast
   6.864 +  with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
   6.865 +    and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
   6.866 +    using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
   6.867 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   6.868 +  with \<open>a \<in># roots p\<close> show ?thesis
   6.869 +    using assms(3)[of a] by auto
   6.870 +qed
   6.871 +
   6.872 +lemma (in field) associated_polynomials_imp_same_roots:
   6.873 +  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
   6.874 +  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots p + roots q"
   6.875 +proof -
   6.876 +  interpret UP: domain "poly_ring R"
   6.877 +    using univ_poly_is_domain[OF carrier_is_subring] .
   6.878 +  from assms show ?thesis
   6.879 +  proof (induction "degree p" arbitrary: p rule: less_induct)
   6.880 +    case less show ?case
   6.881 +    proof (cases "roots p = {#}")
   6.882 +      case True thus ?thesis
   6.883 +        using no_roots_imp_same_roots[of p q] less by simp
   6.884 +    next
   6.885 +      case False with \<open>p \<in> carrier (poly_ring R)\<close>
   6.886 +      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
   6.887 +          and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   6.888 +        by blast
   6.889 +      show ?thesis
   6.890 +      proof (cases "degree p = 1")
   6.891 +        case True with \<open>p \<in> carrier (poly_ring R)\<close>
   6.892 +        obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
   6.893 +          by auto
   6.894 +        with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
   6.895 +          and lead: "lead_coeff p = b" and const: "const_term p = c"
   6.896 +          using degree_one_imp_singleton_roots[of p] less(2) field_Units
   6.897 +          unfolding const_term_def by auto
   6.898 +        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)"
   6.899 +          using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
   6.900 +          by (auto simp add: a lead const)
   6.901 +        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
   6.902 +          using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
   6.903 +        thus ?thesis
   6.904 +          unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
   6.905 +      next
   6.906 +        case False
   6.907 +        from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
   6.908 +        obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
   6.909 +          unfolding pdivides_def by auto
   6.910 +        with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
   6.911 +          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
   6.912 +        with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
   6.913 +          using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
   6.914 +          unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
   6.915 +        with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
   6.916 +          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
   6.917 +        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
   6.918 +          using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
   6.919 +                UP.m_assoc[OF in_carrier r less(4)] p by auto
   6.920 +        also have " ... = add_mset a (roots r + roots q)"
   6.921 +          using less(1)[OF _ r not_zero less(4-5)] deg by simp
   6.922 +        also have " ... = (add_mset a (roots r)) + roots q"
   6.923 +          by simp
   6.924 +        also have " ... = roots p + roots q"
   6.925 +          using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp 
   6.926 +        finally show ?thesis .
   6.927 +      qed
   6.928 +    qed
   6.929 +  qed
   6.930 +qed
   6.931 +
   6.932 +lemma (in field) size_roots_le_degree:
   6.933 +  assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
   6.934 +  using assms
   6.935 +proof (induction "degree p" arbitrary: p rule: less_induct)
   6.936 +  case less show ?case
   6.937 +  proof (cases "roots p = {#}", simp)
   6.938 +    interpret UP: domain "poly_ring R"
   6.939 +      using univ_poly_is_domain[OF carrier_is_subring] .
   6.940 +
   6.941 +    case False with \<open>p \<in> carrier (poly_ring R)\<close>
   6.942 +    obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
   6.943 +      and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   6.944 +      by blast
   6.945 +    then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
   6.946 +      unfolding pdivides_def by auto
   6.947 +    with \<open>a \<in># roots p\<close> have "p \<noteq> []"
   6.948 +      using degree_zero_imp_empty_roots[OF less(2)] by auto
   6.949 +    hence not_zero: "q \<noteq> []"
   6.950 +      using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
   6.951 +    hence "degree p = Suc (degree q)"
   6.952 +      using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
   6.953 +      unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
   6.954 +    with \<open>q \<noteq> []\<close> show ?thesis
   6.955 +      using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
   6.956 +      by (metis Suc_le_mono lessI size_add_mset) 
   6.957 +  qed
   6.958 +qed
   6.959 +
   6.960 +lemma (in domain) pirreducible_roots:
   6.961 +  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
   6.962 +  shows "roots p = {#}"
   6.963 +proof (rule ccontr)
   6.964 +  assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
   6.965 +  obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
   6.966 +    and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   6.967 +    by blast
   6.968 +  hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
   6.969 +    using divides_pirreducible_condition[OF assms(2) in_carrier]
   6.970 +          univ_poly_units_incl[OF carrier_is_subring]
   6.971 +    unfolding pdivides_def by auto
   6.972 +  hence "degree p = 1"
   6.973 +    using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
   6.974 +  with \<open>degree p \<noteq> 1\<close> show False ..
   6.975 +qed
   6.976 +
   6.977 +lemma (in field) pirreducible_imp_not_splitted:
   6.978 +  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
   6.979 +  shows "\<not> splitted p"
   6.980 +  using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
   6.981 +  by (simp add: splitted_def)
   6.982 +
   6.983 +lemma (in field)
   6.984 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
   6.985 +    and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
   6.986 +  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
   6.987 +  using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
   6.988 +  unfolding ring_irreducible_def univ_poly_zero by auto
   6.989 +
   6.990 +lemma (in field) trivial_factors_imp_splitted:
   6.991 +  assumes "p \<in> carrier (poly_ring R)"
   6.992 +    and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
   6.993 +  shows "splitted p"
   6.994 +  using assms
   6.995 +proof (induction "degree p" arbitrary: p rule: less_induct)
   6.996 +  interpret UP: principal_domain "poly_ring R"
   6.997 +    using univ_poly_is_principal[OF carrier_is_subfield] .
   6.998 +  case less show ?case
   6.999 +  proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
  6.1000 +    case False show ?thesis
  6.1001 +    proof (cases "roots p = {#}")
  6.1002 +      case True
  6.1003 +      from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
  6.1004 +        using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
  6.1005 +      then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
  6.1006 +        using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
  6.1007 +      with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
  6.1008 +        using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
  6.1009 +              pdivides_imp_roots_incl[OF _ less(2), of q]
  6.1010 +              pirreducible_degree[OF carrier_is_subfield, of q]
  6.1011 +        by force
  6.1012 +      from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
  6.1013 +        by simp
  6.1014 +      thus ?thesis ..
  6.1015 +    next
  6.1016 +      case False with \<open>p \<in> carrier (poly_ring R)\<close>
  6.1017 +      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
  6.1018 +        and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  6.1019 +        by blast
  6.1020 +      then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
  6.1021 +        unfolding pdivides_def by blast
  6.1022 +      with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
  6.1023 +        by auto
  6.1024 +      with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
  6.1025 +        using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
  6.1026 +      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)"
  6.1027 +        using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
  6.1028 +        unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  6.1029 +      moreover have "q pdivides p"
  6.1030 +        using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
  6.1031 +      hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
  6.1032 +        and "r pdivides q" for r
  6.1033 +        using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
  6.1034 +              pirreducible_degree[OF carrier_is_subfield that(1-2)] 
  6.1035 +        by (auto simp add: pdivides_def)
  6.1036 +      ultimately have "splitted q"
  6.1037 +        using less(1)[OF _ q] by auto
  6.1038 +      with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
  6.1039 +        using poly_mult_degree_one_monic_imp_same_roots[OF a q]
  6.1040 +        unfolding sym[OF p] splitted_def
  6.1041 +        by simp
  6.1042 +    qed
  6.1043 +  qed
  6.1044 +qed
  6.1045 +
  6.1046 +lemma (in field) pdivides_imp_splitted:
  6.1047 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q" 
  6.1048 +  shows "p pdivides q \<Longrightarrow> splitted p"
  6.1049 +proof (cases "p = []")
  6.1050 +  case True thus ?thesis
  6.1051 +    using degree_zero_imp_splitted[OF assms(1)] by simp
  6.1052 +next
  6.1053 +  interpret UP: principal_domain "poly_ring R"
  6.1054 +    using univ_poly_is_principal[OF carrier_is_subfield] .
  6.1055 +
  6.1056 +  case False
  6.1057 +  assume "p pdivides q"
  6.1058 +  then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
  6.1059 +    unfolding pdivides_def by auto
  6.1060 +  with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
  6.1061 +    using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
  6.1062 +  hence "degree p + degree b = size (roots p) + size (roots b)"
  6.1063 +    using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
  6.1064 +          poly_mult_degree_eq[OF carrier_is_subring,of p b]
  6.1065 +    unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
  6.1066 +    by auto
  6.1067 +  moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
  6.1068 +    using size_roots_le_degree assms(1) b by auto
  6.1069 +  ultimately show ?thesis
  6.1070 +    unfolding splitted_def by linarith
  6.1071 +qed
  6.1072 +
  6.1073 +lemma (in field) splitted_imp_trivial_factors:
  6.1074 +  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
  6.1075 +  shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
  6.1076 +  using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
  6.1077 +  by auto 
  6.1078  
  6.1079  
  6.1080  subsection \<open>Link between @{term \<open>(pmod)\<close>} and @{term rupture_surj}\<close>
  6.1081 @@ -970,32 +2020,6 @@
  6.1082    qed
  6.1083  qed
  6.1084  
  6.1085 -(* Move to Ideal.thy ========================================================= *)
  6.1086 -lemma (in ring) quotient_eq_iff_same_a_r_cos:
  6.1087 -  assumes "ideal I R" and "a \<in> carrier R" and "b \<in> carrier R"
  6.1088 -  shows "a \<ominus> b \<in> I \<longleftrightarrow> I +> a = I +> b"
  6.1089 -proof
  6.1090 -  assume "I +> a = I +> b"
  6.1091 -  then obtain i where "i \<in> I" and "\<zero> \<oplus> a = i \<oplus> b"
  6.1092 -    using additive_subgroup.zero_closed[OF ideal.axioms(1)[OF assms(1)]] assms(2)
  6.1093 -    unfolding a_r_coset_def' by blast
  6.1094 -  hence "a \<ominus> b = i"
  6.1095 -    using assms(2-3) by (metis a_minus_def add.inv_solve_right assms(1) ideal.Icarr l_zero)
  6.1096 -  with \<open>i \<in> I\<close> show "a \<ominus> b \<in> I"
  6.1097 -    by simp
  6.1098 -next
  6.1099 -  assume "a \<ominus> b \<in> I"
  6.1100 -  then obtain i where "i \<in> I" and "a = i \<oplus> b"
  6.1101 -    using ideal.Icarr[OF assms(1)] assms(2-3)
  6.1102 -    by (metis a_minus_def add.inv_solve_right)
  6.1103 -  hence "I +> a = (I +> i) +> b"
  6.1104 -    using ideal.Icarr[OF assms(1)] assms(3)
  6.1105 -    by (simp add: a_coset_add_assoc subsetI)
  6.1106 -  with \<open>i \<in> I\<close> show "I +> a = I +> b"
  6.1107 -    using a_rcos_zero[OF assms(1)] by simp
  6.1108 -qed
  6.1109 -(* ========================================================================== *)
  6.1110 -
  6.1111  lemma (in domain) rupture_surj_inj_on:
  6.1112    assumes "subfield K R" and "p \<in> carrier (K[X])"
  6.1113    shows "inj_on (rupture_surj K p) ((\<lambda>q. q pmod p) ` (carrier (K[X])))"
     7.1 --- a/src/HOL/Algebra/Pred_Zorn.thy	Mon Apr 29 17:11:26 2019 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,57 +0,0 @@
     7.4 -theory Pred_Zorn
     7.5 -  imports HOL.Zorn
     7.6 -
     7.7 -begin
     7.8 -
     7.9 -(* ========== *)
    7.10 -lemma partial_order_onE:
    7.11 -  assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
    7.12 -  using assms unfolding partial_order_on_def preorder_on_def by auto
    7.13 -(* ========== *)
    7.14 -
    7.15 -abbreviation rel_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
    7.16 -  where "rel_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
    7.17 -
    7.18 -lemma Field_rel_of:
    7.19 -  assumes "refl_on A (rel_of P A)" shows "Field (rel_of P A) = A"
    7.20 -  using assms unfolding refl_on_def Field_def by auto
    7.21 -
    7.22 -(* ========== *)
    7.23 -lemma Chains_rel_of:
    7.24 -  assumes "C \<in> Chains (rel_of P A)" shows "C \<subseteq> A"
    7.25 -  using assms unfolding Chains_def by auto
    7.26 -(* ========== *)
    7.27 -
    7.28 -lemma partial_order_on_rel_ofI:
    7.29 -  assumes refl: "\<And>a. a \<in> A \<Longrightarrow> P a a"
    7.30 -    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"
    7.31 -    and antisym: "\<And>a b. \<lbrakk> a \<in> A; b \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b a \<Longrightarrow> a = b"
    7.32 -  shows "partial_order_on A (rel_of P A)"
    7.33 -proof -
    7.34 -  from refl have "refl_on A (rel_of P A)"
    7.35 -    unfolding refl_on_def by auto
    7.36 -  moreover have "trans (rel_of P A)" and "antisym (rel_of P A)"
    7.37 -    by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
    7.38 -  ultimately show ?thesis
    7.39 -    unfolding partial_order_on_def preorder_on_def by simp
    7.40 -qed
    7.41 -
    7.42 -lemma Partial_order_rel_ofI:
    7.43 -  assumes "partial_order_on A (rel_of P A)" shows "Partial_order (rel_of P A)"
    7.44 -  using assms unfolding Field_rel_of[OF partial_order_onE(1)[OF assms]] .
    7.45 -
    7.46 -lemma predicate_Zorn:
    7.47 -  assumes "partial_order_on A (rel_of P A)"
    7.48 -    and "\<forall>C \<in> Chains (rel_of P A). \<exists>u \<in> A. \<forall>a \<in> C. P a u"
    7.49 -  shows "\<exists>m \<in> A. \<forall>a \<in> A. P m a \<longrightarrow> a = m"
    7.50 -proof -
    7.51 -  have "a \<in> A" if "a \<in> C" and "C \<in> Chains (rel_of P A)" for C a
    7.52 -    using that Chains_rel_of by auto
    7.53 -  moreover have "(a, u) \<in> rel_of P A" if "a \<in> A" and "u \<in> A" and "P a u" for a u
    7.54 -    using that by auto
    7.55 -  ultimately show ?thesis
    7.56 -    using Zorns_po_lemma[OF Partial_order_rel_ofI[OF assms(1)]] assms(2)
    7.57 -    unfolding Field_rel_of[OF partial_order_onE(1)[OF assms(1)]] by auto
    7.58 -qed
    7.59 -
    7.60 -end
    7.61 \ No newline at end of file