full proof of algebraic closure, by Paulo de Vilhena
authorpaulson <lp15@cam.ac.uk>
Mon Apr 29 16:50:20 2019 +0100 (6 months ago)
changeset 70212e886b58bf698
parent 70196 b7ef9090feed
child 70213 ff8386fc191d
full proof of algebraic closure, by Paulo de Vilhena
src/HOL/Algebra/Algebraic_Closure.thy
     1.1 --- a/src/HOL/Algebra/Algebraic_Closure.thy	Fri Apr 26 16:51:40 2019 +0100
     1.2 +++ b/src/HOL/Algebra/Algebraic_Closure.thy	Mon Apr 29 16:50:20 2019 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  *)
     1.5  
     1.6  theory Algebraic_Closure
     1.7 -  imports Indexed_Polynomials Polynomial_Divisibility Pred_Zorn Finite_Extensions
     1.8 +  imports Indexed_Polynomials Polynomial_Divisibility Finite_Extensions
     1.9  
    1.10  begin
    1.11  
    1.12 @@ -21,18 +21,19 @@
    1.13             \<lparr> mult := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<otimes>\<^bsub>R\<^esub> b),
    1.14                add := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<oplus>\<^bsub>R\<^esub> b) \<rparr>"
    1.15  
    1.16 -definition (in ring) \<sigma> :: "'a list \<Rightarrow> (('a list multiset) \<Rightarrow> 'a) list"
    1.17 +definition (in ring) \<sigma> :: "'a list \<Rightarrow> ((('a list \<times> nat) multiset) \<Rightarrow> 'a) list"
    1.18    where "\<sigma> P = map indexed_const P"
    1.19  
    1.20 -definition (in ring) extensions :: "(('a list multiset) \<Rightarrow> 'a) ring set"
    1.21 +definition (in ring) extensions :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring set"
    1.22    where "extensions \<equiv> { L \<comment> \<open>such that\<close>.
    1.23             \<comment> \<open>i\<close>   (field L) \<and>
    1.24             \<comment> \<open>ii\<close>  (indexed_const \<in> ring_hom R L) \<and>
    1.25             \<comment> \<open>iii\<close> (\<forall>\<P> \<in> carrier L. carrier_coeff \<P>) \<and>
    1.26 -           \<comment> \<open>iv\<close>  (\<forall>\<P> \<in> carrier L. \<forall>P \<in> carrier (poly_ring R).
    1.27 -                       \<not> index_free \<P> P \<longrightarrow> \<X>\<^bsub>P\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>L\<^esub>) }"
    1.28 +           \<comment> \<open>iv\<close>  (\<forall>\<P> \<in> carrier L. \<forall>P \<in> carrier (poly_ring R). \<forall>i.
    1.29 +                       \<not> index_free \<P> (P, i) \<longrightarrow>
    1.30 +                         \<X>\<^bsub>(P, i)\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>L\<^esub>) }"
    1.31  
    1.32 -abbreviation (in ring) restrict_extensions :: "(('a list multiset) \<Rightarrow> 'a) ring set" ("\<S>")
    1.33 +abbreviation (in ring) restrict_extensions :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring set" ("\<S>")
    1.34    where "\<S> \<equiv> law_restrict ` extensions"
    1.35  
    1.36  
    1.37 @@ -65,7 +66,7 @@
    1.38  lemma (in field) law_restrict_is_field: "field (law_restrict R)"
    1.39  proof -
    1.40    have "comm_monoid_axioms (law_restrict R)"
    1.41 -    using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto 
    1.42 +    using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto
    1.43    then interpret L: cring "law_restrict R"
    1.44      using cring.intro law_restrict_is_ring comm_monoid.intro ring.is_monoid by auto
    1.45    have "Units R = Units (law_restrict R)"
    1.46 @@ -73,7 +74,7 @@
    1.47    thus ?thesis
    1.48      using L.cring_fieldI unfolding field_Units law_restrict_carrier law_restrict_zero by simp
    1.49  qed
    1.50 -    
    1.51 +
    1.52  lemma law_restrict_iso_imp_eq:
    1.53    assumes "id \<in> ring_iso (law_restrict A) (law_restrict B)" and "ring A" and "ring B"
    1.54    shows "law_restrict A = law_restrict B"
    1.55 @@ -112,38 +113,38 @@
    1.56  
    1.57  subsection \<open>Partial Order\<close>
    1.58  
    1.59 -lemma iso_incl_backwards: 
    1.60 +lemma iso_incl_backwards:
    1.61    assumes "A \<lesssim> B" shows "id \<in> ring_hom A B"
    1.62    using assms by cases
    1.63  
    1.64 -lemma iso_incl_antisym_aux: 
    1.65 +lemma iso_incl_antisym_aux:
    1.66    assumes "A \<lesssim> B" and "B \<lesssim> A" shows "id \<in> ring_iso A B"
    1.67 -proof - 
    1.68 -  have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A" 
    1.69 +proof -
    1.70 +  have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A"
    1.71      using assms(1-2)[THEN iso_incl_backwards] by auto
    1.72 -  thus ?thesis 
    1.73 +  thus ?thesis
    1.74      using hom[THEN ring_hom_memE(1)] by (auto simp add: ring_iso_def bij_betw_def inj_on_def)
    1.75  qed
    1.76  
    1.77 -lemma iso_incl_refl: "A \<lesssim> A" 
    1.78 +lemma iso_incl_refl: "A \<lesssim> A"
    1.79    by (rule iso_inclI[OF ring_hom_memI], auto)
    1.80  
    1.81 -lemma iso_incl_trans: 
    1.82 +lemma iso_incl_trans:
    1.83    assumes "A \<lesssim> B" and "B \<lesssim> C" shows "A \<lesssim> C"
    1.84    using ring_hom_trans[OF assms[THEN iso_incl_backwards]] by auto
    1.85  
    1.86  lemma (in ring) iso_incl_antisym:
    1.87    assumes "A \<in> \<S>" "B \<in> \<S>" and "A \<lesssim> B" "B \<lesssim> A" shows "A = B"
    1.88 -proof - 
    1.89 -  obtain A' B' :: "('a list multiset \<Rightarrow> 'a) ring" 
    1.90 +proof -
    1.91 +  obtain A' B' :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring"
    1.92      where A: "A = law_restrict A'" "ring A'" and B: "B = law_restrict B'" "ring B'"
    1.93      using assms(1-2) field.is_ring by (auto simp add: extensions_def)
    1.94 -  thus ?thesis 
    1.95 +  thus ?thesis
    1.96      using law_restrict_iso_imp_eq iso_incl_antisym_aux[OF assms(3-4)] by simp
    1.97  qed
    1.98  
    1.99 -lemma (in ring) iso_incl_partial_order: "partial_order_on \<S> (rel_of (\<lesssim>) \<S>)"
   1.100 -  using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_rel_ofI)
   1.101 +lemma (in ring) iso_incl_partial_order: "partial_order_on \<S> (relation_of (\<lesssim>) \<S>)"
   1.102 +  using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_relation_ofI)
   1.103  
   1.104  lemma iso_inclE:
   1.105    assumes "ring A" and "ring B" and "A \<lesssim> B" shows "ring_hom_ring A B id"
   1.106 @@ -174,14 +175,14 @@
   1.107      show "indexed_const \<in> ring_hom R (image_ring indexed_const R)"
   1.108        using inj_imp_image_ring_iso[OF indexed_const_inj_on] unfolding ring_iso_def by auto
   1.109    next
   1.110 -    fix \<P> :: "('a list multiset) \<Rightarrow> 'a" and P
   1.111 +    fix \<P> :: "(('a list \<times> nat) multiset) \<Rightarrow> 'a" and P and i
   1.112      assume "\<P> \<in> carrier (image_ring indexed_const R)"
   1.113      then obtain k where "k \<in> carrier R" and "\<P> = indexed_const k"
   1.114        unfolding image_ring_carrier by blast
   1.115 -    hence "index_free \<P> P" for P
   1.116 +    hence "index_free \<P> (P, i)" for P i
   1.117        unfolding index_free_def indexed_const_def by auto
   1.118 -    thus "\<not> index_free \<P> P \<Longrightarrow> \<X>\<^bsub>P\<^esub> \<in> carrier (image_ring indexed_const R)"
   1.119 -     and "\<not> index_free \<P> P \<Longrightarrow> ring.eval (image_ring indexed_const R) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>image_ring indexed_const R\<^esub>"
   1.120 +    thus "\<not> index_free \<P> (P, i) \<Longrightarrow> \<X>\<^bsub>(P, i)\<^esub> \<in> carrier (image_ring indexed_const R)"
   1.121 +     and "\<not> index_free \<P> (P, i) \<Longrightarrow> ring.eval (image_ring indexed_const R) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>image_ring indexed_const R\<^esub>"
   1.122        by auto
   1.123      from \<open>k \<in> carrier R\<close> and \<open>\<P> = indexed_const k\<close> show "carrier_coeff \<P>"
   1.124        unfolding indexed_const_def carrier_coeff_def by auto
   1.125 @@ -194,7 +195,7 @@
   1.126  subsection \<open>Chains\<close>
   1.127  
   1.128  definition union_ring :: "(('a, 'c) ring_scheme) set \<Rightarrow> 'a ring"
   1.129 -  where "union_ring C = 
   1.130 +  where "union_ring C =
   1.131             \<lparr> carrier = (\<Union>(carrier ` C)),
   1.132           monoid.mult = (\<lambda>a b. (monoid.mult (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b)),
   1.133                   one = one (SOME R. R \<in> C),
   1.134 @@ -281,7 +282,7 @@
   1.135      using field_chain by simp
   1.136  
   1.137    show "a \<otimes>\<^bsub>union_ring C\<^esub> b \<in> carrier (union_ring C)"
   1.138 -    using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto 
   1.139 +    using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto
   1.140    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)"
   1.141     and "a \<otimes>\<^bsub>union_ring C\<^esub> b = b \<otimes>\<^bsub>union_ring C\<^esub> a"
   1.142     and "\<one>\<^bsub>union_ring C\<^esub> \<otimes>\<^bsub>union_ring C\<^esub> a = a"
   1.143 @@ -290,7 +291,7 @@
   1.144  next
   1.145    show "\<one>\<^bsub>union_ring C\<^esub> \<in> carrier (union_ring C)"
   1.146      using ring.ring_simprules(6)[OF ring_chain] assms same_one_same_zero(1)
   1.147 -    unfolding union_ring_carrier by auto    
   1.148 +    unfolding union_ring_carrier by auto
   1.149  qed
   1.150  
   1.151  lemma union_ring_is_abelian_group:
   1.152 @@ -308,7 +309,7 @@
   1.153    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)"
   1.154     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)"
   1.155     and "a \<oplus>\<^bsub>union_ring C\<^esub> b = b \<oplus>\<^bsub>union_ring C\<^esub> a"
   1.156 -   and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a" 
   1.157 +   and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a"
   1.158      using same_one_same_zero[OF R(1)] same_laws[OF R(1)] R(2-4) l_distr a_assoc a_comm by auto
   1.159    have "\<exists>a' \<in> carrier R. a' \<oplus>\<^bsub>union_ring C\<^esub> a = \<zero>\<^bsub>union_ring C\<^esub>"
   1.160      using same_laws(2)[OF R(1)] R(2) same_one_same_zero[OF R(1)] by simp
   1.161 @@ -334,7 +335,7 @@
   1.162        using field_chain by simp
   1.163  
   1.164      from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>\<close> have "a \<in> Units R"
   1.165 -      unfolding same_one_same_zero[OF R(1)] field_Units by auto 
   1.166 +      unfolding same_one_same_zero[OF R(1)] field_Units by auto
   1.167      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>"
   1.168        using same_laws[OF R(1)] same_one_same_zero[OF R(1)] R(2) unfolding Units_def by auto
   1.169      with \<open>R \<in> C\<close> and \<open>a \<in> carrier (union_ring C)\<close> show "a \<in> Units (union_ring C)"
   1.170 @@ -370,78 +371,84 @@
   1.171  
   1.172  subsection \<open>Zorn\<close>
   1.173  
   1.174 +(* ========== *)
   1.175 +lemma Chains_relation_of:
   1.176 +  assumes "C \<in> Chains (relation_of P A)" shows "C \<subseteq> A"
   1.177 +  using assms unfolding Chains_def relation_of_def by auto
   1.178 +(* ========== *)
   1.179 +
   1.180  lemma (in ring) exists_core_chain:
   1.181 -  assumes "C \<in> Chains (rel_of (\<lesssim>) \<S>)" obtains C' where "C' \<subseteq> extensions" and "C = law_restrict ` C'"
   1.182 -  using Chains_rel_of[OF assms] by (meson subset_image_iff)
   1.183 +  assumes "C \<in> Chains (relation_of (\<lesssim>) \<S>)" obtains C' where "C' \<subseteq> extensions" and "C = law_restrict ` C'"
   1.184 +  using Chains_relation_of[OF assms] by (meson subset_image_iff)
   1.185  
   1.186  lemma (in ring) core_chain_is_chain:
   1.187 -  assumes "law_restrict ` C \<in> Chains (rel_of (\<lesssim>) \<S>)" shows "\<And>R S. \<lbrakk> R \<in> C; S \<in> C \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
   1.188 +  assumes "law_restrict ` C \<in> Chains (relation_of (\<lesssim>) \<S>)" shows "\<And>R S. \<lbrakk> R \<in> C; S \<in> C \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
   1.189  proof -
   1.190    fix R S assume "R \<in> C" and "S \<in> C" thus "R \<lesssim> S \<or> S \<lesssim> R"
   1.191 -    using assms(1) unfolding iso_incl_hom[of R] iso_incl_hom[of S] Chains_def by auto
   1.192 +    using assms(1) unfolding iso_incl_hom[of R] iso_incl_hom[of S] Chains_def relation_of_def
   1.193 +    by auto
   1.194  qed
   1.195  
   1.196  lemma (in field) exists_maximal_extension:
   1.197    shows "\<exists>M \<in> \<S>. \<forall>L \<in> \<S>. M \<lesssim> L \<longrightarrow> L = M"
   1.198  proof (rule predicate_Zorn[OF iso_incl_partial_order])
   1.199 -  show "\<forall>C \<in> Chains (rel_of (\<lesssim>) \<S>). \<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
   1.200 -  proof
   1.201 -    fix C assume C: "C \<in> Chains (rel_of (\<lesssim>) \<S>)"
   1.202 -    show "\<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
   1.203 -    proof (cases)
   1.204 -      assume "C = {}" thus ?thesis
   1.205 -        using extensions_non_empty by auto
   1.206 -    next
   1.207 -      assume "C \<noteq> {}"
   1.208 -      from \<open>C \<in> Chains (rel_of (\<lesssim>) \<S>)\<close>
   1.209 -      obtain C' where C': "C' \<subseteq> extensions" "C = law_restrict ` C'"
   1.210 -        using exists_core_chain by auto
   1.211 -      with \<open>C \<noteq> {}\<close> obtain S where S: "S \<in> C'" and "C' \<noteq> {}"
   1.212 -        by auto
   1.213 +  fix C assume C: "C \<in> Chains (relation_of (\<lesssim>) \<S>)"
   1.214 +  show "\<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
   1.215 +  proof (cases)
   1.216 +    assume "C = {}" thus ?thesis
   1.217 +      using extensions_non_empty by auto
   1.218 +  next
   1.219 +    assume "C \<noteq> {}"
   1.220 +    from \<open>C \<in> Chains (relation_of (\<lesssim>) \<S>)\<close>
   1.221 +    obtain C' where C': "C' \<subseteq> extensions" "C = law_restrict ` C'"
   1.222 +      using exists_core_chain by auto
   1.223 +    with \<open>C \<noteq> {}\<close> obtain S where S: "S \<in> C'" and "C' \<noteq> {}"
   1.224 +      by auto
   1.225  
   1.226 -      have core_chain: "\<And>R. R \<in> C' \<Longrightarrow> field R" "\<And>R S. \<lbrakk> R \<in> C'; S \<in> C' \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
   1.227 -        using core_chain_is_chain[of C'] C' C unfolding extensions_def by auto
   1.228 -      from \<open>C' \<noteq> {}\<close> interpret Union: field "union_ring C'"
   1.229 -          using union_ring_is_field[OF core_chain] C'(1) by blast
   1.230 +    have core_chain: "\<And>R. R \<in> C' \<Longrightarrow> field R" "\<And>R S. \<lbrakk> R \<in> C'; S \<in> C' \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
   1.231 +      using core_chain_is_chain[of C'] C' C unfolding extensions_def by auto
   1.232 +    from \<open>C' \<noteq> {}\<close> interpret Union: field "union_ring C'"
   1.233 +        using union_ring_is_field[OF core_chain] C'(1) by blast
   1.234  
   1.235 -      have "union_ring C' \<in> extensions"
   1.236 -      proof (auto simp add: extensions_def)
   1.237 -        show "field (union_ring C')"
   1.238 -          using Union.field_axioms .
   1.239 -      next
   1.240 -        from \<open>S \<in> C'\<close> have "indexed_const \<in> ring_hom R S"
   1.241 -          using C'(1) unfolding extensions_def by auto
   1.242 -        thus "indexed_const \<in> ring_hom R (union_ring C')"
   1.243 -          using ring_hom_trans[of _ R S id] union_ring_is_upper_bound[OF core_chain S]
   1.244 -          unfolding iso_incl.simps by auto
   1.245 -      next
   1.246 -        show "a \<in> carrier (union_ring C') \<Longrightarrow> carrier_coeff a" for a
   1.247 -          using C'(1) unfolding union_ring_carrier extensions_def by auto
   1.248 -      next
   1.249 -        fix \<P> P
   1.250 -        assume "\<P> \<in> carrier (union_ring C')" and P: "P \<in> carrier (poly_ring R)" "\<not> index_free \<P> P"
   1.251 -        from \<open>\<P> \<in> carrier (union_ring C')\<close> obtain T where T: "T \<in> C'" "\<P> \<in> carrier T"
   1.252 -          using exists_superset_carrier[of C' "{ \<P> }"] core_chain by auto
   1.253 -        hence "\<X>\<^bsub>P\<^esub> \<in> carrier T" and "(ring.eval T) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>T\<^esub>"
   1.254 -          and field: "field T" and hom: "indexed_const \<in> ring_hom R T"
   1.255 -          using P C'(1) unfolding extensions_def by auto
   1.256 -        with \<open>T \<in> C'\<close> show "\<X>\<^bsub>P\<^esub> \<in> carrier (union_ring C')"
   1.257 -          unfolding union_ring_carrier by auto
   1.258 -        have "set P \<subseteq> carrier R"
   1.259 -          using P(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.260 -        hence "set (\<sigma> P) \<subseteq> carrier T"
   1.261 -          using ring_hom_memE(1)[OF hom] unfolding \<sigma>_def by (induct P) (auto)
   1.262 -        with \<open>\<X>\<^bsub>P\<^esub> \<in> carrier T\<close> and \<open>(ring.eval T) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>T\<^esub>\<close>
   1.263 -        show "(ring.eval (union_ring C')) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>union_ring C'\<^esub>"
   1.264 -          using iso_incl_imp_same_eval[OF field.is_ring[OF field] Union.is_ring
   1.265 -                union_ring_is_upper_bound[OF core_chain T(1)]] same_one_same_zero(2)[OF core_chain T(1)]
   1.266 -          by auto
   1.267 -      qed
   1.268 -      moreover have "R \<lesssim> law_restrict (union_ring C')" if "R \<in> C" for R
   1.269 -        using that union_ring_is_upper_bound[OF core_chain] iso_incl_hom unfolding C' by auto
   1.270 -      ultimately show ?thesis
   1.271 -        by blast
   1.272 +    have "union_ring C' \<in> extensions"
   1.273 +    proof (auto simp add: extensions_def)
   1.274 +      show "field (union_ring C')"
   1.275 +        using Union.field_axioms .
   1.276 +    next
   1.277 +      from \<open>S \<in> C'\<close> have "indexed_const \<in> ring_hom R S"
   1.278 +        using C'(1) unfolding extensions_def by auto
   1.279 +      thus "indexed_const \<in> ring_hom R (union_ring C')"
   1.280 +        using ring_hom_trans[of _ R S id] union_ring_is_upper_bound[OF core_chain S]
   1.281 +        unfolding iso_incl.simps by auto
   1.282 +    next
   1.283 +      show "a \<in> carrier (union_ring C') \<Longrightarrow> carrier_coeff a" for a
   1.284 +        using C'(1) unfolding union_ring_carrier extensions_def by auto
   1.285 +    next
   1.286 +      fix \<P> P i
   1.287 +      assume "\<P> \<in> carrier (union_ring C')"
   1.288 +        and P: "P \<in> carrier (poly_ring R)"
   1.289 +        and not_index_free: "\<not> index_free \<P> (P, i)"
   1.290 +      from \<open>\<P> \<in> carrier (union_ring C')\<close> obtain T where T: "T \<in> C'" "\<P> \<in> carrier T"
   1.291 +        using exists_superset_carrier[of C' "{ \<P> }"] core_chain by auto
   1.292 +      hence "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier T" and "(ring.eval T) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>T\<^esub>"
   1.293 +        and field: "field T" and hom: "indexed_const \<in> ring_hom R T"
   1.294 +        using P not_index_free C'(1) unfolding extensions_def by auto
   1.295 +      with \<open>T \<in> C'\<close> show "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier (union_ring C')"
   1.296 +        unfolding union_ring_carrier by auto
   1.297 +      have "set P \<subseteq> carrier R"
   1.298 +        using P unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.299 +      hence "set (\<sigma> P) \<subseteq> carrier T"
   1.300 +        using ring_hom_memE(1)[OF hom] unfolding \<sigma>_def by (induct P) (auto)
   1.301 +      with \<open>\<X>\<^bsub>(P, i)\<^esub> \<in> carrier T\<close> and \<open>(ring.eval T) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>T\<^esub>\<close>
   1.302 +      show "(ring.eval (union_ring C')) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>union_ring C'\<^esub>"
   1.303 +        using iso_incl_imp_same_eval[OF field.is_ring[OF field] Union.is_ring
   1.304 +              union_ring_is_upper_bound[OF core_chain T(1)]] same_one_same_zero(2)[OF core_chain T(1)]
   1.305 +        by auto
   1.306      qed
   1.307 +    moreover have "R \<lesssim> law_restrict (union_ring C')" if "R \<in> C" for R
   1.308 +      using that union_ring_is_upper_bound[OF core_chain] iso_incl_hom unfolding C' by auto
   1.309 +    ultimately show ?thesis
   1.310 +      by blast
   1.311    qed
   1.312  qed
   1.313  
   1.314 @@ -461,11 +468,11 @@
   1.315    hence "set (map h p) \<subseteq> carrier S"
   1.316      by (induct p) (auto)
   1.317    moreover have "h a = \<zero>\<^bsub>S\<^esub> \<Longrightarrow> a = \<zero>\<^bsub>R\<^esub>" if "a \<in> carrier R" for a
   1.318 -    using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp 
   1.319 +    using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp
   1.320    with \<open>set p \<subseteq> carrier R\<close> have "lead_coeff (map h p) \<noteq> \<zero>\<^bsub>S\<^esub>" if "p \<noteq> []"
   1.321      using lc[OF that] that by (cases p) (auto)
   1.322    ultimately show ?thesis
   1.323 -    unfolding sym[OF univ_poly_carrier] polynomial_def by auto 
   1.324 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.325  qed
   1.326  
   1.327  lemma (in ring_hom_ring) subfield_polynomial_hom:
   1.328 @@ -485,44 +492,1252 @@
   1.329      using S.univ_poly_consistent[OF subfieldE(1)[OF img_is_subfield(2)[OF assms]]] by simp
   1.330  qed
   1.331  
   1.332 +
   1.333 +(* MOVE ========== *)
   1.334 +subsection \<open>Roots and Multiplicity\<close>
   1.335 +
   1.336 +definition (in ring) is_root :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
   1.337 +  where "is_root p x \<longleftrightarrow> (x \<in> carrier R \<and> eval p x = \<zero> \<and> p \<noteq> [])"
   1.338 +
   1.339 +definition (in ring) alg_mult :: "'a list \<Rightarrow> 'a \<Rightarrow> nat"
   1.340 +  where "alg_mult p x =
   1.341 +           (if p = [] then 0 else
   1.342 +             (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"
   1.343 +
   1.344 +definition (in ring) roots :: "'a list \<Rightarrow> 'a multiset"
   1.345 +  where "roots p = Abs_multiset (alg_mult p)"
   1.346 +
   1.347 +definition (in ring) roots_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> 'a multiset"
   1.348 +  where "roots_on K p = roots p \<inter># mset_set K"
   1.349 +
   1.350 +definition (in ring) splitted :: "'a list \<Rightarrow> bool"
   1.351 +  where "splitted p \<longleftrightarrow> size (roots p) = degree p"
   1.352 +
   1.353 +definition (in ring) splitted_on :: "'a set \<Rightarrow> 'a list \<Rightarrow> bool"
   1.354 +  where "splitted_on K p \<longleftrightarrow> size (roots_on K p) = degree p"
   1.355 +
   1.356 +lemma (in domain) polynomial_pow_not_zero:
   1.357 +  assumes "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
   1.358 +  shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \<noteq> []"
   1.359 +proof -
   1.360 +  interpret UP: domain "poly_ring R"
   1.361 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.362 +
   1.363 +  from assms UP.integral show ?thesis
   1.364 +    unfolding sym[OF univ_poly_zero[of R "carrier R"]]
   1.365 +    by (induction n, auto)
   1.366 +qed
   1.367 +
   1.368 +lemma (in domain) subring_polynomial_pow_not_zero:
   1.369 +  assumes "subring K R" and "p \<in> carrier (K[X])" and "p \<noteq> []"
   1.370 +  shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \<noteq> []"
   1.371 +  using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
   1.372 +  unfolding univ_poly_consistent[OF assms(1)] by simp
   1.373 +
   1.374 +lemma (in domain) polynomial_pow_degree:
   1.375 +  assumes "p \<in> carrier (poly_ring R)"
   1.376 +  shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
   1.377 +proof -
   1.378 +  interpret UP: domain "poly_ring R"
   1.379 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.380 +
   1.381 +  show ?thesis
   1.382 +  proof (induction n)
   1.383 +    case 0 thus ?case
   1.384 +      using UP.nat_pow_0 unfolding univ_poly_one by auto
   1.385 +  next
   1.386 +    let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
   1.387 +    case (Suc n) thus ?case
   1.388 +    proof (cases "p = []")
   1.389 +      case True thus ?thesis
   1.390 +        using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
   1.391 +    next
   1.392 +      case False
   1.393 +      hence "?ppow n \<in> carrier (poly_ring R)" and "?ppow n \<noteq> []" and "p \<noteq> []"
   1.394 +        using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
   1.395 +      thus ?thesis
   1.396 +        using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
   1.397 +        unfolding univ_poly_carrier univ_poly_zero
   1.398 +        by (auto simp add: add.commute univ_poly_mult)
   1.399 +    qed
   1.400 +  qed
   1.401 +qed
   1.402 +
   1.403 +lemma (in domain) polynomial_pow_division:
   1.404 +  assumes "p \<in> carrier (poly_ring R)" and "(n::nat) \<le> m"
   1.405 +  shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
   1.406 +proof -
   1.407 +  interpret UP: domain "poly_ring R"
   1.408 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.409 +
   1.410 +  let ?ppow = "\<lambda>n. p [^]\<^bsub>poly_ring R\<^esub> n"
   1.411 +
   1.412 +  have "?ppow n \<otimes>\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
   1.413 +    using assms(1) by (simp add: UP.nat_pow_mult)
   1.414 +  thus ?thesis
   1.415 +    using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
   1.416 +    unfolding pdivides_def by auto
   1.417 +qed
   1.418 +
   1.419 +lemma (in domain) degree_zero_imp_not_is_root:
   1.420 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "\<not> is_root p x"
   1.421 +proof (cases "p = []", simp add: is_root_def)
   1.422 +  case False with \<open>degree p = 0\<close> have "length p = Suc 0"
   1.423 +    using le_SucE by fastforce
   1.424 +  then obtain a where "p = [ a ]" and "a \<in> carrier R" and "a \<noteq> \<zero>"
   1.425 +    using assms unfolding sym[OF univ_poly_carrier] polynomial_def
   1.426 +    by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
   1.427 +  thus ?thesis
   1.428 +    unfolding is_root_def by auto
   1.429 +qed
   1.430 +
   1.431 +lemma (in domain) is_root_imp_pdivides:
   1.432 +  assumes "p \<in> carrier (poly_ring R)"
   1.433 +  shows "is_root p x \<Longrightarrow> [ \<one>, \<ominus> x ] pdivides p"
   1.434 +proof -
   1.435 +  let ?b = "[ \<one> , \<ominus> x ]"
   1.436 +
   1.437 +  interpret UP: domain "poly_ring R"
   1.438 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.439 +
   1.440 +  assume "is_root p x" hence x: "x \<in> carrier R" and is_root: "eval p x = \<zero>"
   1.441 +    unfolding is_root_def by auto
   1.442 +  hence b: "?b \<in> carrier (poly_ring R)"
   1.443 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.444 +  then obtain q r where q: "q \<in> carrier (poly_ring R)" and r: "r \<in> carrier (poly_ring R)"
   1.445 +    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"
   1.446 +    using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)
   1.447 +
   1.448 +  show ?thesis
   1.449 +  proof (cases "r = []")
   1.450 +    case True then have "r = \<zero>\<^bsub>poly_ring R\<^esub>"
   1.451 +      unfolding univ_poly_zero[of R "carrier R"] .
   1.452 +    thus ?thesis
   1.453 +      using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
   1.454 +  next
   1.455 +    case False then have "length r = Suc 0"
   1.456 +      using long_divides(2) le_SucE by fastforce
   1.457 +    then obtain a where "r = [ a ]" and a: "a \<in> carrier R" and "a \<noteq> \<zero>"
   1.458 +      using r unfolding sym[OF univ_poly_carrier] polynomial_def
   1.459 +      by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))
   1.460 +
   1.461 +    have "eval p x = ((eval ?b x) \<otimes> (eval q x)) \<oplus> (eval r x)"
   1.462 +      using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
   1.463 +    also have " ... = eval r x"
   1.464 +      using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
   1.465 +    finally have "a = \<zero>"
   1.466 +      using a unfolding \<open>r = [ a ]\<close> is_root by simp
   1.467 +    with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
   1.468 +  qed
   1.469 +qed
   1.470 +
   1.471 +lemma (in domain) pdivides_imp_is_root:
   1.472 +  assumes "p \<noteq> []" and "x \<in> carrier R"
   1.473 +  shows "[ \<one>, \<ominus> x ] pdivides p \<Longrightarrow> is_root p x"
   1.474 +proof -
   1.475 +  assume "[ \<one>, \<ominus> x ] pdivides p"
   1.476 +  then obtain q where q: "q \<in> carrier (poly_ring R)" and pdiv: "p = [ \<one>, \<ominus> x ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
   1.477 +    unfolding pdivides_def by auto
   1.478 +  moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   1.479 +    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   1.480 +  ultimately have "eval p x = \<zero>"
   1.481 +    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
   1.482 +  with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
   1.483 +    unfolding is_root_def by simp
   1.484 +qed
   1.485 +
   1.486 +(* MOVE TO Polynomial_Dvisibility.thy ================== *)
   1.487 +lemma (in domain) associated_polynomials_imp_same_length: (* stronger than "imp_same_degree" *)
   1.488 +  assumes "subring K R" and "p \<in> carrier (K[X])" and "q \<in> carrier (K[X])"
   1.489 +  shows "p \<sim>\<^bsub>K[X]\<^esub> q \<Longrightarrow> length p = length q"
   1.490 +proof -
   1.491 +  { fix p q
   1.492 +    assume p: "p \<in> carrier (K[X])" and q: "q \<in> carrier (K[X])" and "p \<sim>\<^bsub>K[X]\<^esub> q"
   1.493 +    have "length p \<le> length q"
   1.494 +    proof (cases "q = []")
   1.495 +      case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []"
   1.496 +        unfolding associated_def True factor_def univ_poly_def by auto
   1.497 +      thus ?thesis
   1.498 +        using True by simp
   1.499 +    next
   1.500 +      case False
   1.501 +      from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p divides\<^bsub>K [X]\<^esub> q"
   1.502 +        unfolding associated_def by simp
   1.503 +      hence "p divides\<^bsub>poly_ring R\<^esub> q"
   1.504 +        using carrier_polynomial[OF assms(1)]
   1.505 +        unfolding factor_def univ_poly_carrier univ_poly_mult by auto
   1.506 +      with \<open>q \<noteq> []\<close> have "degree p \<le> degree q"
   1.507 +        using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
   1.508 +      with \<open>q \<noteq> []\<close> show ?thesis
   1.509 +        by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
   1.510 +    qed
   1.511 +  } note aux_lemma = this
   1.512 +
   1.513 +  interpret UP: domain "K[X]"
   1.514 +    using univ_poly_is_domain[OF assms(1)] .
   1.515 +
   1.516 +  assume "p \<sim>\<^bsub>K[X]\<^esub> q" thus ?thesis
   1.517 +    using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp
   1.518 +qed
   1.519 +(* ================================================= *)
   1.520 +
   1.521 +lemma (in domain) associated_polynomials_imp_same_is_root:
   1.522 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
   1.523 +  shows "is_root p x \<longleftrightarrow> is_root q x"
   1.524 +proof (cases "p = []")
   1.525 +  case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
   1.526 +    unfolding associated_def True factor_def univ_poly_def by auto
   1.527 +  thus ?thesis
   1.528 +    using True unfolding is_root_def by simp
   1.529 +next
   1.530 +  case False
   1.531 +  interpret UP: domain "poly_ring R"
   1.532 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.533 +
   1.534 +  { fix p q
   1.535 +    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"
   1.536 +    have "is_root p x \<Longrightarrow> is_root q x"
   1.537 +    proof -
   1.538 +      assume is_root: "is_root p x"
   1.539 +      then have "[ \<one>, \<ominus> x ] pdivides p" and "p \<noteq> []" and "x \<in> carrier R"
   1.540 +        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
   1.541 +      moreover have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   1.542 +        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
   1.543 +      ultimately have "[ \<one>, \<ominus> x ] pdivides q"
   1.544 +        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
   1.545 +      with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show ?thesis
   1.546 +        using associated_polynomials_imp_same_length[OF carrier_is_subring p q pq]
   1.547 +              pdivides_imp_is_root[of q x]
   1.548 +        by fastforce
   1.549 +    qed
   1.550 +  }
   1.551 +
   1.552 +  then show ?thesis
   1.553 +    using assms UP.associated_sym[OF assms(3)] by blast
   1.554 +qed
   1.555 +
   1.556 +lemma (in ring) monic_degree_one_root_condition:
   1.557 +  assumes "a \<in> carrier R" shows "is_root [ \<one>, \<ominus> a ] b \<longleftrightarrow> a = b"
   1.558 +  using assms minus_equality r_neg[OF assms] unfolding is_root_def by (auto, fastforce)
   1.559 +
   1.560 +lemma (in field) degree_one_root_condition:
   1.561 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
   1.562 +  shows "is_root p x \<longleftrightarrow> x = \<ominus> (inv (lead_coeff p) \<otimes> (const_term p))"
   1.563 +proof -
   1.564 +  interpret UP: domain "poly_ring R"
   1.565 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.566 +
   1.567 +  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
   1.568 +    by simp
   1.569 +  then obtain a b where p: "p = [ a, b ]"
   1.570 +    by (metis length_0_conv length_Cons list.exhaust nat.inject)
   1.571 +  hence a: "a \<in> carrier R" "a \<noteq> \<zero>" and b: "b \<in> carrier R"
   1.572 +    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.573 +  hence inv_a: "inv a \<in> carrier R" "(inv a) \<otimes> a = \<one>"
   1.574 +    using subfield_m_inv[OF carrier_is_subfield, of a] by auto
   1.575 +  hence in_carrier: "[ \<one>, (inv a) \<otimes> b ] \<in> carrier (poly_ring R)"
   1.576 +    using b unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.577 +
   1.578 +  have "p \<sim>\<^bsub>poly_ring R\<^esub> [ \<one>, (inv a) \<otimes> b ]"
   1.579 +  proof (rule UP.associatedI2'[OF _ _ in_carrier, of _ "[ a ]"])
   1.580 +    have "p = [ a ] \<otimes>\<^bsub>poly_ring R\<^esub> [ \<one>, inv a \<otimes> b ]"
   1.581 +      using a inv_a b m_assoc[of a "inv a" b] unfolding p univ_poly_mult by (auto, algebra)
   1.582 +    also have " ... = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]"
   1.583 +      using UP.m_comm[OF in_carrier, of "[ a ]"] a
   1.584 +      by (auto simp add: sym[OF univ_poly_carrier] polynomial_def)
   1.585 +    finally show "p = [ \<one>, inv a \<otimes> b ] \<otimes>\<^bsub>poly_ring R\<^esub> [ a ]" .
   1.586 +  next
   1.587 +    from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<close> show "[ a ] \<in> Units (poly_ring R)"
   1.588 +      unfolding univ_poly_units[OF carrier_is_subfield] by simp
   1.589 +  qed
   1.590 +
   1.591 +  moreover have "(inv a) \<otimes> b = \<ominus> (\<ominus> (inv (lead_coeff p) \<otimes> (const_term p)))"
   1.592 +    and "inv (lead_coeff p) \<otimes> (const_term p) \<in> carrier R"
   1.593 +    using inv_a a b unfolding p const_term_def by auto
   1.594 +
   1.595 +  ultimately show ?thesis
   1.596 +    using associated_polynomials_imp_same_is_root[OF assms(1) in_carrier]
   1.597 +          monic_degree_one_root_condition
   1.598 +    by (metis add.inv_closed)
   1.599 +qed
   1.600 +
   1.601 +lemma (in domain) is_root_imp_is_root_poly_mult:
   1.602 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "q \<noteq> []"
   1.603 +  shows "is_root p x \<Longrightarrow> is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
   1.604 +proof -
   1.605 +  interpret UP: domain "poly_ring R"
   1.606 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.607 +
   1.608 +  assume "is_root p x" then have x: "x \<in> carrier R" and eval: "eval p x = \<zero>" and not_zero: "p \<noteq> []"
   1.609 +    unfolding is_root_def by simp+
   1.610 +  hence "p \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
   1.611 +    using assms UP.integral unfolding sym[OF univ_poly_zero[of R "carrier R"]] by blast
   1.612 +  moreover have "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
   1.613 +    using assms eval ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by auto
   1.614 +  ultimately show ?thesis
   1.615 +    using x unfolding is_root_def by simp
   1.616 +qed
   1.617 +
   1.618 +lemma (in domain) is_root_poly_mult_imp_is_root:
   1.619 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
   1.620 +  shows "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x \<Longrightarrow> (is_root p x) \<or> (is_root q x)"
   1.621 +proof -
   1.622 +  interpret UP: domain "poly_ring R"
   1.623 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.624 +
   1.625 +  assume is_root: "is_root (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x"
   1.626 +  hence "p \<noteq> []" and "q \<noteq> []"
   1.627 +    unfolding is_root_def sym[OF univ_poly_zero[of R "carrier R"]]
   1.628 +    using UP.l_null[OF assms(2)] UP.r_null[OF assms(1)] by blast+
   1.629 +  moreover have x: "x \<in> carrier R" and "eval (p \<otimes>\<^bsub>poly_ring R\<^esub> q) x = \<zero>"
   1.630 +    using is_root unfolding is_root_def by simp+
   1.631 +  hence "eval p x = \<zero> \<or> eval q x = \<zero>"
   1.632 +    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring], of x] assms integral by auto
   1.633 +  ultimately show "(is_root p x) \<or> (is_root q x)"
   1.634 +    using x unfolding is_root_def by auto
   1.635 +qed
   1.636 +
   1.637 +(*
   1.638 +lemma (in domain)
   1.639 +  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
   1.640 +  shows "pprime K p"
   1.641 +proof (rule pprimeI[OF assms(1-2)])
   1.642 +  from \<open>degree p = 1\<close> show "p \<noteq> []" and "p \<notin> Units (K [X])"
   1.643 +    unfolding univ_poly_units[OF assms(1)] by auto
   1.644 +next
   1.645 +  fix q r
   1.646 +  assume "q \<in> carrier (K[X])" and "r \<in> carrier (K[X])"
   1.647 +    and pdiv: "p pdivides q \<otimes>\<^bsub>K [X]\<^esub> r"
   1.648 +  hence "q \<in> carrier (poly_ring R)" and "r \<in> carrier (poly_ring R)"
   1.649 +    using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
   1.650 +  moreover obtain b where b: "b \<in>"
   1.651 +qed
   1.652 +*)
   1.653 +
   1.654 +lemma (in domain) finite_number_of_roots:
   1.655 +  assumes "p \<in> carrier (poly_ring R)" shows "finite { x. is_root p x }"
   1.656 +  using assms
   1.657 +proof (induction "degree p" arbitrary: p)
   1.658 +  case 0 thus ?case
   1.659 +    by (simp add: degree_zero_imp_not_is_root)
   1.660 +next
   1.661 +  case (Suc n) show ?case
   1.662 +  proof (cases "{ x. is_root p x } = {}")
   1.663 +    case True thus ?thesis
   1.664 +      by (simp add: True)
   1.665 +  next
   1.666 +    interpret UP: domain "poly_ring R"
   1.667 +      using univ_poly_is_domain[OF carrier_is_subring] .
   1.668 +
   1.669 +    case False
   1.670 +    then obtain a where is_root: "is_root p a"
   1.671 +      by blast
   1.672 +    hence a: "a \<in> carrier R" and eval: "eval p a = \<zero>" and p_not_zero: "p \<noteq> []"
   1.673 +      unfolding is_root_def by auto
   1.674 +    hence in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
   1.675 +      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.676 +
   1.677 +    obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
   1.678 +      using is_root_imp_pdivides[OF Suc(3) is_root] unfolding pdivides_def by auto
   1.679 +    with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
   1.680 +      using UP.r_null UP.integral in_carrier unfolding sym[OF univ_poly_zero[of R "carrier R"]]
   1.681 +      by metis
   1.682 +    hence "degree q = n"
   1.683 +      using poly_mult_degree_eq[OF carrier_is_subring, of "[ \<one>, \<ominus> a ]" q]
   1.684 +            in_carrier q p_not_zero p Suc(2)
   1.685 +      unfolding univ_poly_carrier
   1.686 +      by (metis One_nat_def Suc_eq_plus1 diff_Suc_1 list.distinct(1)
   1.687 +                list.size(3-4) plus_1_eq_Suc univ_poly_mult)
   1.688 +    hence "finite { x. is_root q x }"
   1.689 +      using Suc(1)[OF _ q] by simp
   1.690 +
   1.691 +    moreover have "{ x. is_root p x } \<subseteq> insert a { x. is_root q x }"
   1.692 +      using is_root_poly_mult_imp_is_root[OF in_carrier q]
   1.693 +            monic_degree_one_root_condition[OF a]
   1.694 +      unfolding p by auto
   1.695 +
   1.696 +    ultimately show ?thesis
   1.697 +      using finite_subset by auto
   1.698 +  qed
   1.699 +qed
   1.700 +
   1.701 +lemma (in domain) alg_multE:
   1.702 +  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)" and "p \<noteq> []"
   1.703 +  shows "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
   1.704 +    and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
   1.705 +proof -
   1.706 +  interpret UP: domain "poly_ring R"
   1.707 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.708 +
   1.709 +  let ?ppow = "\<lambda>n :: nat. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n)"
   1.710 +
   1.711 +  define S :: "nat set" where "S = { n. ?ppow n pdivides p }"
   1.712 +  have "?ppow 0 = \<one>\<^bsub>poly_ring R\<^esub>"
   1.713 +    using UP.nat_pow_0 by simp
   1.714 +  hence "0 \<in> S"
   1.715 +    using UP.one_divides[OF assms(2)] unfolding S_def pdivides_def by simp
   1.716 +  hence "S \<noteq> {}"
   1.717 +    by auto
   1.718 +
   1.719 +  moreover have "n \<le> degree p" if "n \<in> S" for n :: nat
   1.720 +  proof -
   1.721 +    have "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   1.722 +      using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.723 +    hence "?ppow n \<in> carrier (poly_ring R)"
   1.724 +      using assms unfolding univ_poly_zero by auto
   1.725 +    with \<open>n \<in> S\<close> have "degree (?ppow n) \<le> degree p"
   1.726 +      using pdivides_imp_degree_le[OF carrier_is_subring _ assms(2-3), of "?ppow n"] by (simp add: S_def)
   1.727 +    with \<open>[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)\<close> show ?thesis
   1.728 +      using polynomial_pow_degree by simp
   1.729 +  qed
   1.730 +  hence "finite S"
   1.731 +    using finite_nat_set_iff_bounded_le by blast
   1.732 +
   1.733 +  ultimately have MaxS: "\<And>n. n \<in> S \<Longrightarrow> n \<le> Max S" "Max S \<in> S"
   1.734 +    using Max_ge[of S] Max_in[of S] by auto
   1.735 +  with \<open>x \<in> carrier R\<close> have "alg_mult p x = Max S"
   1.736 +    using Greatest_equality[of "\<lambda>n. ?ppow n pdivides p" "Max S"] assms(3)
   1.737 +    unfolding S_def alg_mult_def by auto
   1.738 +  thus "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x)) pdivides p"
   1.739 +   and "\<And>n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p \<Longrightarrow> n \<le> alg_mult p x"
   1.740 +    using MaxS unfolding S_def by auto
   1.741 +qed
   1.742 +
   1.743 +lemma (in domain) le_alg_mult_imp_pdivides:
   1.744 +  assumes "x \<in> carrier R" and "p \<in> carrier (poly_ring R)"
   1.745 +  shows "n \<le> alg_mult p x \<Longrightarrow> ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p"
   1.746 +proof -
   1.747 +  interpret UP: domain "poly_ring R"
   1.748 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.749 +
   1.750 +  assume le_alg_mult: "n \<le> alg_mult p x"
   1.751 +  have in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   1.752 +    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.753 +  hence ppow_pdivides:
   1.754 +    "([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides
   1.755 +     ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p x))"
   1.756 +    using polynomial_pow_division[OF _ le_alg_mult] by simp
   1.757 +
   1.758 +  show ?thesis
   1.759 +  proof (cases "p = []")
   1.760 +    case True thus ?thesis
   1.761 +      using in_carrier pdivides_zero[OF carrier_is_subring] by auto
   1.762 +  next
   1.763 +    case False thus ?thesis
   1.764 +      using ppow_pdivides UP.divides_trans UP.nat_pow_closed alg_multE(1)[OF assms] in_carrier
   1.765 +      unfolding pdivides_def by meson
   1.766 +  qed
   1.767 +qed
   1.768 +
   1.769 +lemma (in domain) alg_mult_gt_zero_iff_is_root:
   1.770 +  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p x > 0 \<longleftrightarrow> is_root p x"
   1.771 +proof -
   1.772 +  interpret UP: domain "poly_ring R"
   1.773 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.774 +  show ?thesis
   1.775 +  proof
   1.776 +    assume is_root: "is_root p x" hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
   1.777 +      unfolding is_root_def by auto
   1.778 +    have "[\<one>, \<ominus> x] [^]\<^bsub>poly_ring R\<^esub> (Suc 0) = [\<one>, \<ominus> x]"
   1.779 +      using x unfolding univ_poly_def by auto
   1.780 +    thus "alg_mult p x > 0"
   1.781 +      using is_root_imp_pdivides[OF _ is_root] alg_multE(2)[OF x, of p "Suc 0"] not_zero assms by auto
   1.782 +  next
   1.783 +    assume gt_zero: "alg_mult p x > 0"
   1.784 +    hence x: "x \<in> carrier R" and not_zero: "p \<noteq> []"
   1.785 +      unfolding alg_mult_def by (cases "p = []", auto, cases "x \<in> carrier R", auto)
   1.786 +    hence in_carrier: "[ \<one>, \<ominus> x ] \<in> carrier (poly_ring R)"
   1.787 +      unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.788 +    with \<open>x \<in> carrier R\<close> have "[ \<one>, \<ominus> x ] pdivides p" and "eval [ \<one>, \<ominus> x ] x = \<zero>"
   1.789 +      using le_alg_mult_imp_pdivides[of x p "1::nat"] gt_zero assms by (auto, algebra)
   1.790 +    thus "is_root p x"
   1.791 +      using pdivides_imp_root_sharing[OF in_carrier] not_zero x by (simp add: is_root_def)
   1.792 +  qed
   1.793 +qed
   1.794 +
   1.795 +lemma (in domain) alg_mult_in_multiset:
   1.796 +  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p \<in> multiset"
   1.797 +  using assms alg_mult_gt_zero_iff_is_root finite_number_of_roots unfolding multiset_def by auto
   1.798 +
   1.799 +lemma (in domain) alg_mult_eq_count_roots:
   1.800 +  assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
   1.801 +  using alg_mult_in_multiset[OF assms] by (simp add: roots_def)
   1.802 +
   1.803 +lemma (in domain) roots_mem_iff_is_root:
   1.804 +  assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
   1.805 +  using alg_mult_eq_count_roots[OF assms] count_greater_zero_iff
   1.806 +  unfolding roots_def sym[OF alg_mult_gt_zero_iff_is_root[OF assms]] by metis
   1.807 +
   1.808 +lemma (in domain) degree_zero_imp_empty_roots:
   1.809 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "roots p = {#}"
   1.810 +proof -
   1.811 +  have "alg_mult p = (\<lambda>x. 0)"
   1.812 +  proof (cases "p = []")
   1.813 +    case True thus ?thesis
   1.814 +      using assms unfolding alg_mult_def by auto
   1.815 +  next
   1.816 +    case False hence "length p = Suc 0"
   1.817 +      using assms(2) by (simp add: le_Suc_eq)
   1.818 +    then obtain a where "a \<in> carrier R" and "a \<noteq> \<zero>" and p: "p = [ a ]"
   1.819 +      using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def
   1.820 +      by (metis Suc_length_conv hd_in_set length_0_conv list.sel(1) subset_code(1))
   1.821 +    show ?thesis
   1.822 +    proof (rule ccontr)
   1.823 +      assume "alg_mult p \<noteq> (\<lambda>x. 0)"
   1.824 +      then obtain x where "alg_mult p x > 0"
   1.825 +        by auto
   1.826 +      with \<open>p \<noteq> []\<close> have "eval p x = \<zero>"
   1.827 +        using alg_mult_gt_zero_iff_is_root[OF assms(1), of x] unfolding is_root_def by simp
   1.828 +      with \<open>a \<in> carrier R\<close> have "a = \<zero>"
   1.829 +        unfolding p by auto
   1.830 +      with \<open>a \<noteq> \<zero>\<close> show False ..
   1.831 +    qed
   1.832 +  qed
   1.833 +  thus ?thesis
   1.834 +    by (simp add: roots_def zero_multiset.abs_eq)
   1.835 +qed
   1.836 +
   1.837 +lemma (in domain) degree_zero_imp_splitted:
   1.838 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 0" shows "splitted p"
   1.839 +  unfolding splitted_def degree_zero_imp_empty_roots[OF assms] assms(2) by simp
   1.840 +
   1.841 +lemma (in domain) roots_inclI':
   1.842 +  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"
   1.843 +  shows "roots p \<subseteq># m"
   1.844 +proof (intro mset_subset_eqI)
   1.845 +  fix a show "count (roots p) a \<le> count m a"
   1.846 +    using assms unfolding sym[OF alg_mult_eq_count_roots[OF assms(1)]] alg_mult_def
   1.847 +    by (cases "p = []", simp, cases "a \<in> carrier R", auto)
   1.848 +qed
   1.849 +
   1.850 +lemma (in domain) roots_inclI:
   1.851 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
   1.852 +    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"
   1.853 +  shows "roots p \<subseteq># roots q"
   1.854 +  using roots_inclI'[OF assms(1), of "roots q"] assms alg_multE(2)[OF _ assms(2-3)]
   1.855 +  unfolding sym[OF alg_mult_eq_count_roots[OF assms(2)]] by auto
   1.856 +
   1.857 +lemma (in domain) pdivides_imp_roots_incl:
   1.858 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
   1.859 +  shows "p pdivides q \<Longrightarrow> roots p \<subseteq># roots q"
   1.860 +proof (rule roots_inclI[OF assms])
   1.861 +  interpret UP: domain "poly_ring R"
   1.862 +    using univ_poly_is_domain[OF carrier_is_subring] .
   1.863 +
   1.864 +  fix a assume "p pdivides q" and a: "a \<in> carrier R"
   1.865 +  hence "[ \<one> , \<ominus> a ] \<in> carrier (poly_ring R)"
   1.866 +    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
   1.867 +  with \<open>p pdivides q\<close> show "([\<one>, \<ominus> a] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a)) pdivides q"
   1.868 +    using UP.divides_trans[of _p q] le_alg_mult_imp_pdivides[OF a assms(1)]
   1.869 +    by (auto simp add: pdivides_def)
   1.870 +qed
   1.871 +
   1.872 +lemma (in domain) associated_polynomials_imp_same_roots:
   1.873 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" and "p \<sim>\<^bsub>poly_ring R\<^esub> q"
   1.874 +  shows "roots p = roots q"
   1.875 +  using assms pdivides_imp_roots_incl zero_pdivides
   1.876 +  unfolding pdivides_def associated_def
   1.877 +  by (metis subset_mset.eq_iff)
   1.878 +
   1.879 +(* MOVE to Polynomial_Divisibility.thy *)
   1.880 +lemma (in comm_monoid_cancel) prime_pow_divides_iff:
   1.881 +  assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)"
   1.882 +  shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b"
   1.883 +proof
   1.884 +  assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)"
   1.885 +    using divides_prod_l[of "p [^] n" b a] assms by simp
   1.886 +next
   1.887 +  assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b"
   1.888 +  proof (induction n)
   1.889 +    case 0 with \<open>b \<in> carrier G\<close> show ?case
   1.890 +      by (simp add: unit_divides)
   1.891 +  next
   1.892 +    case (Suc n)
   1.893 +    hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b"
   1.894 +      using assms(1) divides_prod_r by auto
   1.895 +    with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d
   1.896 +      where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c"
   1.897 +        and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d"
   1.898 +      using assms by blast
   1.899 +    hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)"
   1.900 +      using assms by (simp add: m_assoc m_lcomm)
   1.901 +    hence "a \<otimes> c = p \<otimes> d"
   1.902 +      using c d assms(1) assms(2) l_cancel by blast
   1.903 +    with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c"
   1.904 +      by (metis assms(2) c d dividesI' prime_divides)
   1.905 +    with \<open>b = (p [^] n) \<otimes> c\<close> show ?case
   1.906 +      using assms(1) c by simp
   1.907 +  qed
   1.908 +qed
   1.909 +
   1.910 +(* MOVE to Polynomial_Divisibility.thy *)
   1.911 +lemma (in domain) pirreducible_pow_pdivides_iff:
   1.912 +  assumes "subfield K R" "p \<in> carrier (K[X])" "q \<in> carrier (K[X])" "r \<in> carrier (K[X])"
   1.913 +    and "pirreducible K p" and "\<not> (p pdivides q)"
   1.914 +  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"
   1.915 +proof -
   1.916 +  interpret UP: principal_domain "K[X]"
   1.917 +    using univ_poly_is_principal[OF assms(1)] .
   1.918 +  show ?thesis
   1.919 +  proof (cases "r = []")
   1.920 +    case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
   1.921 +      unfolding  sym[OF univ_poly_zero[of R K]] by auto
   1.922 +    thus ?thesis
   1.923 +      using pdivides_zero[OF subfieldE(1),of K] assms by auto
   1.924 +  next
   1.925 +    case False then have not_zero: "p \<noteq> []" "q \<noteq> []" "r \<noteq> []" "q \<otimes>\<^bsub>K[X]\<^esub> r \<noteq> []"
   1.926 +      using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
   1.927 +            UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
   1.928 +    from \<open>p \<noteq> []\<close>
   1.929 +    have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<noteq> []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \<in> carrier (K[X])"
   1.930 +      using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
   1.931 +    have not_pdiv: "\<not> (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
   1.932 +      using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
   1.933 +    have prime: "prime (mult_of (K[X])) p"
   1.934 +      using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
   1.935 +      unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
   1.936 +    have "a pdivides b \<longleftrightarrow> a divides\<^bsub>mult_of (K[X])\<^esub> b"
   1.937 +      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
   1.938 +      using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
   1.939 +      unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
   1.940 +    thus ?thesis
   1.941 +      using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
   1.942 +      unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
   1.943 +      by (metis DiffI UP.m_closed singletonD)
   1.944 +  qed
   1.945 +qed
   1.946 +
   1.947 +(* MOVE to Polynomial_Divisibility.thy *)
   1.948 +lemma (in domain) univ_poly_units':
   1.949 +  assumes "subfield K R" shows "p \<in> Units (K[X]) \<longleftrightarrow> p \<in> carrier (K[X]) \<and> p \<noteq> [] \<and> degree p = 0"
   1.950 +  unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
   1.951 +  by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)
   1.952 +
   1.953 +(* MOVE to Polynomial_Divisibility.thy *)
   1.954 +lemma (in domain) subring_degree_one_imp_pirreducible:
   1.955 +  assumes "subring K R" and "a \<in> Units (R \<lparr> carrier := K \<rparr>)" and "b \<in> K"
   1.956 +  shows "pirreducible K [ a, b ]"
   1.957 +proof (rule pirreducibleI[OF assms(1)])
   1.958 +  have "a \<in> K" and "a \<noteq> \<zero>"
   1.959 +    using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
   1.960 +  thus "[ a, b ] \<in> carrier (K[X])" and "[ a, b ] \<noteq> []" and "[ a, b ] \<notin> Units (K [X])"
   1.961 +    using univ_poly_units_incl[OF assms(1)] assms(2-3)
   1.962 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.963 +next
   1.964 +  interpret UP: domain "K[X]"
   1.965 +    using univ_poly_is_domain[OF assms(1)] .
   1.966 +
   1.967 +  { fix q r
   1.968 +    assume q: "q \<in> carrier (K[X])" and r: "r \<in> carrier (K[X])" and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r"
   1.969 +    hence not_zero: "q \<noteq> []" "r \<noteq> []"
   1.970 +      by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
   1.971 +    have "degree (q \<otimes>\<^bsub>K[X]\<^esub> r) = degree q + degree r"
   1.972 +      using not_zero poly_mult_degree_eq[OF assms(1)] q r
   1.973 +      by (simp add: univ_poly_carrier univ_poly_mult)
   1.974 +    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> []"
   1.975 +      using not_zero by auto
   1.976 +  } note aux_lemma1 = this
   1.977 +
   1.978 +  { fix q r
   1.979 +    assume q: "q \<in> carrier (K[X])" "q \<noteq> []" and r: "r \<in> carrier (K[X])" "r \<noteq> []"
   1.980 +      and "[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
   1.981 +    hence "length q = Suc (Suc 0)" and "length r = Suc 0"
   1.982 +      by (linarith, metis add.right_neutral add_eq_if length_0_conv)
   1.983 +    from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
   1.984 +      by (metis length_0_conv length_Cons list.exhaust nat.inject)
   1.985 +    from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
   1.986 +      by (metis length_0_conv length_Suc_conv)
   1.987 +    from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
   1.988 +    have c: "c \<in> K" "c \<noteq> \<zero>" and d: "d \<in> K" and e: "e \<in> K" "e \<noteq> \<zero>"
   1.989 +      using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
   1.990 +    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
   1.991 +      using poly_mult_lead_coeff[OF assms(1), of q r]
   1.992 +      unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
   1.993 +    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>"
   1.994 +      using assms(2) unfolding Units_def by auto
   1.995 +    hence "a \<noteq> \<zero>" and "inv_a \<noteq> \<zero>"
   1.996 +      using subringE(1)[OF assms(1)] integral_iff by auto
   1.997 +    with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
   1.998 +      using subringE(1,6)[OF assms(1)] inv_a integral
   1.999 +      unfolding sym[OF univ_poly_carrier] polynomial_def
  1.1000 +      by (auto, meson subsetD)
  1.1001 +    moreover have "[ c \<otimes> inv_a ] \<otimes>\<^bsub>K[X]\<^esub> r = [ \<one> ]"
  1.1002 +      using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
  1.1003 +      unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
  1.1004 +    ultimately have "r \<in> Units (K[X])"
  1.1005 +      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
  1.1006 +  } note aux_lemma2 = this
  1.1007 +
  1.1008 +  fix q r
  1.1009 +  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"
  1.1010 +  thus "q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
  1.1011 +    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
  1.1012 +qed
  1.1013 +
  1.1014 +(* MOVE to Polynomial_Divisibility.thy *)
  1.1015 +lemma (in domain) degree_one_imp_pirreducible:
  1.1016 +  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
  1.1017 +  shows "pirreducible K p"
  1.1018 +proof -
  1.1019 +  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
  1.1020 +    by simp
  1.1021 +  then obtain a b where p: "p = [ a, b ]"
  1.1022 +    by (metis length_0_conv length_Suc_conv)
  1.1023 +  with \<open>p \<in> carrier (K[X])\<close> show ?thesis
  1.1024 +    using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
  1.1025 +          subfield.subfield_Units[OF assms(1)]
  1.1026 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1027 +qed
  1.1028 +
  1.1029 +(* MOVE to Polynomial_Divisibility.thy *)
  1.1030 +lemma (in ring) degree_oneE[elim]:
  1.1031 +  assumes "p \<in> carrier (K[X])" and "degree p = 1"
  1.1032 +    and "\<And>a b. \<lbrakk> a \<in> K; a \<noteq> \<zero>; b \<in> K; p = [ a, b ] \<rbrakk> \<Longrightarrow> P"
  1.1033 +  shows P
  1.1034 +proof -
  1.1035 +  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
  1.1036 +    by simp
  1.1037 +  then obtain a b where "p = [ a, b ]"
  1.1038 +    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
  1.1039 +  with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
  1.1040 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1041 +  with \<open>p = [ a, b ]\<close> show ?thesis
  1.1042 +    using assms(3) by simp
  1.1043 +qed
  1.1044 +
  1.1045 +(* MOVE to Polynomial_Divisibility.thy *)
  1.1046 +lemma (in domain) subring_degree_one_associatedI:
  1.1047 +  assumes "subring K R" and "a \<in> K" "a' \<in> K" and "b \<in> K" and "a \<otimes> a' = \<one>"
  1.1048 +  shows "[ a , b ] \<sim>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
  1.1049 +proof -
  1.1050 +  from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
  1.1051 +    using subringE(1)[OF assms(1)] assms(2-3) by auto
  1.1052 +  hence "[ a, b ] = [ a ] \<otimes>\<^bsub>K[X]\<^esub> [ \<one>, a' \<otimes> b ]"
  1.1053 +    using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
  1.1054 +    unfolding univ_poly_mult by fastforce
  1.1055 +  moreover have "[ a, b ] \<in> carrier (K[X])" and "[ \<one>, a' \<otimes> b ] \<in> carrier (K[X])"
  1.1056 +    using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
  1.1057 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1058 +  moreover have "[ a ] \<in> Units (K[X])"
  1.1059 +  proof -
  1.1060 +    from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
  1.1061 +      using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1062 +    moreover have "a' \<otimes> a = \<one>"
  1.1063 +      using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp
  1.1064 +    hence "[ a ] \<otimes>\<^bsub>K[X]\<^esub> [ a' ] = [ \<one> ]" and "[ a' ] \<otimes>\<^bsub>K[X]\<^esub> [ a ] = [ \<one> ]"
  1.1065 +      using assms unfolding univ_poly_mult by auto
  1.1066 +    ultimately show ?thesis
  1.1067 +      unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
  1.1068 +  qed
  1.1069 +  ultimately show ?thesis
  1.1070 +    using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
  1.1071 +qed
  1.1072 +
  1.1073 +(* MOVE to Polynomial_Divisibility.thy *)
  1.1074 +lemma (in domain) degree_one_associatedI:
  1.1075 +  assumes "subfield K R" and "p \<in> carrier (K[X])" and "degree p = 1"
  1.1076 +  shows "p \<sim>\<^bsub>K[X]\<^esub> [ \<one>, inv (lead_coeff p) \<otimes> (const_term p) ]"
  1.1077 +proof -
  1.1078 +  from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
  1.1079 +  obtain a b where "p = [ a, b ]" and "a \<in> K" "a \<noteq> \<zero>" and "b \<in> K"
  1.1080 +    by auto
  1.1081 +  thus ?thesis
  1.1082 +    using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
  1.1083 +          subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
  1.1084 +    unfolding const_term_def
  1.1085 +    by auto
  1.1086 +qed
  1.1087 +
  1.1088 +lemma (in domain) monic_degree_one_roots:
  1.1089 +  assumes "a \<in> carrier R" shows "roots [ \<one> , \<ominus> a ] = {# a #}"
  1.1090 +proof -
  1.1091 +  let ?p = "[ \<one> , \<ominus> a ]"
  1.1092 +
  1.1093 +  interpret UP: domain "poly_ring R"
  1.1094 +    using univ_poly_is_domain[OF carrier_is_subring] .
  1.1095 +
  1.1096 +  from \<open>a \<in> carrier R\<close> have in_carrier: "?p \<in> carrier (poly_ring R)"
  1.1097 +    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  1.1098 +  show ?thesis
  1.1099 +  proof (rule subset_mset.antisym)
  1.1100 +    show "{# a #} \<subseteq># roots ?p"
  1.1101 +      using roots_mem_iff_is_root[OF in_carrier]
  1.1102 +            monic_degree_one_root_condition[OF assms]
  1.1103 +      by simp
  1.1104 +  next
  1.1105 +    show "roots ?p \<subseteq># {# a #}"
  1.1106 +    proof (rule mset_subset_eqI, auto)
  1.1107 +      fix b assume "a \<noteq> b" thus "count (roots ?p) b = 0"
  1.1108 +        using alg_mult_gt_zero_iff_is_root[OF in_carrier]
  1.1109 +              monic_degree_one_root_condition[OF assms]
  1.1110 +        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
  1.1111 +        by fastforce
  1.1112 +    next
  1.1113 +      have "(?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) pdivides ?p"
  1.1114 +        using le_alg_mult_imp_pdivides[OF assms in_carrier] by simp
  1.1115 +      hence "degree (?p [^]\<^bsub>poly_ring R\<^esub> (alg_mult ?p a)) \<le> degree ?p"
  1.1116 +        using pdivides_imp_degree_le[OF carrier_is_subring, of _ ?p] in_carrier by auto
  1.1117 +      thus "count (roots ?p) a \<le> Suc 0"
  1.1118 +        using polynomial_pow_degree[OF in_carrier]
  1.1119 +        unfolding sym[OF alg_mult_eq_count_roots[OF in_carrier]]
  1.1120 +        by auto
  1.1121 +    qed
  1.1122 +  qed
  1.1123 +qed
  1.1124 +
  1.1125 +lemma (in domain) degree_one_roots:
  1.1126 +  assumes "a \<in> carrier R" "a' \<in> carrier R" and "b \<in> carrier R" and "a \<otimes> a' = \<one>"
  1.1127 +  shows "roots [ a , b ] = {# \<ominus> (a' \<otimes> b) #}"
  1.1128 +proof -
  1.1129 +  have "[ a, b ] \<in> carrier (poly_ring R)" and "[ \<one>, a' \<otimes> b ] \<in> carrier (poly_ring R)"
  1.1130 +    using assms unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1131 +  thus ?thesis
  1.1132 +    using subring_degree_one_associatedI[OF carrier_is_subring assms] assms
  1.1133 +          monic_degree_one_roots associated_polynomials_imp_same_roots
  1.1134 +    by (metis add.inv_closed local.minus_minus m_closed)
  1.1135 +qed
  1.1136 +
  1.1137 +lemma (in field) degree_one_imp_singleton_roots:
  1.1138 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1"
  1.1139 +  shows "roots p = {# \<ominus> (inv (lead_coeff p) \<otimes> (const_term p)) #}"
  1.1140 +proof -
  1.1141 +  from \<open>p \<in> carrier (poly_ring R)\<close> and \<open>degree p = 1\<close>
  1.1142 +  obtain a b where "p = [ a, b ]" and "a \<in> carrier R" "a \<noteq> \<zero>" and "b \<in> carrier R"
  1.1143 +    by auto
  1.1144 +  thus ?thesis
  1.1145 +    using degree_one_roots[of a "inv a" b]
  1.1146 +    by (auto simp add: const_term_def field_Units)
  1.1147 +qed
  1.1148 +
  1.1149 +lemma (in field) degree_one_imp_splitted:
  1.1150 +  assumes "p \<in> carrier (poly_ring R)" and "degree p = 1" shows "splitted p"
  1.1151 +  using degree_one_imp_singleton_roots[OF assms] assms(2) unfolding splitted_def by simp
  1.1152 +
  1.1153 +lemma (in field) no_roots_imp_same_roots:
  1.1154 +  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)"
  1.1155 +  shows "roots p = {#} \<Longrightarrow> roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
  1.1156 +proof -
  1.1157 +  interpret UP: domain "poly_ring R"
  1.1158 +    using univ_poly_is_domain[OF carrier_is_subring] .
  1.1159 +
  1.1160 +  assume no_roots: "roots p = {#}" show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
  1.1161 +  proof (intro subset_mset.antisym)
  1.1162 +    have pdiv: "q pdivides (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
  1.1163 +      using UP.divides_prod_l assms unfolding pdivides_def by blast
  1.1164 +    show "roots q \<subseteq># roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q)"
  1.1165 +      using pdivides_imp_roots_incl[OF _ _ _ pdiv] assms
  1.1166 +            degree_zero_imp_empty_roots[OF assms(3)]
  1.1167 +      by (cases "q = []", auto, metis UP.l_null UP.m_rcancel UP.zero_closed univ_poly_zero)
  1.1168 +  next
  1.1169 +    show "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) \<subseteq># roots q"
  1.1170 +    proof (cases "p \<otimes>\<^bsub>poly_ring R\<^esub> q = []")
  1.1171 +      case True thus ?thesis
  1.1172 +        using degree_zero_imp_empty_roots[OF UP.m_closed[OF assms(1,3)]] by simp
  1.1173 +    next
  1.1174 +      case False with \<open>p \<noteq> []\<close> have q_not_zero: "q \<noteq> []"
  1.1175 +        by (metis UP.r_null assms(1) univ_poly_zero)
  1.1176 +      show ?thesis
  1.1177 +      proof (rule roots_inclI[OF UP.m_closed[OF assms(1,3)] assms(3) q_not_zero])
  1.1178 +        fix a assume a: "a \<in> carrier R"
  1.1179 +        hence "\<not> ([ \<one>, \<ominus> a ] pdivides p)"
  1.1180 +          using assms(1-2) no_roots pdivides_imp_is_root roots_mem_iff_is_root[of p] by auto
  1.1181 +        moreover have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  1.1182 +          using a unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1183 +        hence "pirreducible (carrier R) [ \<one>, \<ominus> a ]"
  1.1184 +          using degree_one_imp_pirreducible[OF carrier_is_subfield] by simp
  1.1185 +        moreover
  1.1186 +        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)"
  1.1187 +          using le_alg_mult_imp_pdivides[OF a UP.m_closed, of p q] assms by simp
  1.1188 +        ultimately show "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult (p \<otimes>\<^bsub>poly_ring R\<^esub> q) a)) pdivides q"
  1.1189 +          using pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier] assms by auto
  1.1190 +      qed
  1.1191 +    qed
  1.1192 +  qed
  1.1193 +qed
  1.1194 +
  1.1195 +lemma (in field) poly_mult_degree_one_monic_imp_same_roots:
  1.1196 +  assumes "a \<in> carrier R" and "p \<in> carrier (poly_ring R)" "p \<noteq> []"
  1.1197 +  shows "roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) = add_mset a (roots p)"
  1.1198 +proof -
  1.1199 +  interpret UP: domain "poly_ring R"
  1.1200 +    using univ_poly_is_domain[OF carrier_is_subring] .
  1.1201 +
  1.1202 +  from \<open>a \<in> carrier R\<close> have in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  1.1203 +    unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  1.1204 +
  1.1205 +  show ?thesis
  1.1206 +  proof (intro subset_mset.antisym[OF roots_inclI' mset_subset_eqI])
  1.1207 +    show "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) \<in> carrier (poly_ring R)"
  1.1208 +      using in_carrier assms(2) by simp
  1.1209 +  next
  1.1210 +    fix b assume b: "b \<in> carrier R" and "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
  1.1211 +    hence not_zero: "p \<noteq> []"
  1.1212 +      unfolding univ_poly_def by auto
  1.1213 +    from \<open>b \<in> carrier R\<close> have in_carrier':  "[ \<one>, \<ominus> b ] \<in> carrier (poly_ring R)"
  1.1214 +      unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  1.1215 +    show "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b \<le> count (add_mset a (roots p)) b"
  1.1216 +    proof (cases "a = b")
  1.1217 +      case False
  1.1218 +      hence "\<not> [ \<one>, \<ominus> b ] pdivides [ \<one>, \<ominus> a ]"
  1.1219 +        using assms(1) b monic_degree_one_root_condition pdivides_imp_is_root by blast
  1.1220 +      moreover have "pirreducible (carrier R) [ \<one>, \<ominus> b ]"
  1.1221 +        using degree_one_imp_pirreducible[OF carrier_is_subfield in_carrier'] by simp
  1.1222 +      ultimately
  1.1223 +      have "[ \<one>, \<ominus> b ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) b) pdivides p"
  1.1224 +        using le_alg_mult_imp_pdivides[OF b UP.m_closed, of _ p] assms(2) in_carrier
  1.1225 +              pirreducible_pow_pdivides_iff[OF carrier_is_subfield in_carrier' in_carrier, of p]
  1.1226 +        by auto
  1.1227 +      with \<open>a \<noteq> b\<close> show ?thesis
  1.1228 +        using alg_mult_eq_count_roots[OF assms(2)] alg_multE(2)[OF b assms(2) not_zero] by auto
  1.1229 +    next
  1.1230 +      case True
  1.1231 +      have "[ \<one>, \<ominus> a ] pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
  1.1232 +        using dividesI[OF assms(2)] unfolding pdivides_def by auto
  1.1233 +      with \<open>[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []\<close>
  1.1234 +      have "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a \<ge> Suc 0"
  1.1235 +        using alg_multE(2)[of a _ "Suc 0"] in_carrier assms by auto
  1.1236 +      then obtain m where m: "alg_mult ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p) a = Suc m"
  1.1237 +        using Suc_le_D by blast
  1.1238 +      hence "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m)) pdivides
  1.1239 +             ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
  1.1240 +        using le_alg_mult_imp_pdivides[OF _ UP.m_closed, of a _ p]
  1.1241 +              in_carrier assms UP.nat_pow_Suc2 by force
  1.1242 +      hence "([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> m) pdivides p"
  1.1243 +        using UP.mult_divides in_carrier assms(2)
  1.1244 +        unfolding univ_poly_zero pdivides_def factor_def
  1.1245 +        by (simp add: UP.m_assoc UP.m_lcancel univ_poly_zero)
  1.1246 +      with \<open>a = b\<close> show ?thesis
  1.1247 +        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
  1.1248 +              alg_multE(2)[OF assms(1) _ not_zero] m
  1.1249 +        by auto
  1.1250 +    qed
  1.1251 +  next
  1.1252 +    fix b
  1.1253 +    have not_zero: "[ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p \<noteq> []"
  1.1254 +      using assms in_carrier univ_poly_zero[of R] UP.integral by auto
  1.1255 +
  1.1256 +    show "count (add_mset a (roots p)) b \<le> count (roots ([\<one>, \<ominus> a] \<otimes>\<^bsub>poly_ring R\<^esub> p)) b"
  1.1257 +    proof (cases "a = b")
  1.1258 +      case True
  1.1259 +      have "([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> ([ \<one>, \<ominus> a ] [^]\<^bsub>poly_ring R\<^esub> (alg_mult p a))) pdivides
  1.1260 +            ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
  1.1261 +        using UP.divides_mult[OF _ in_carrier] le_alg_mult_imp_pdivides[OF assms(1,2)] in_carrier assms
  1.1262 +        by (auto simp add: pdivides_def)
  1.1263 +      with \<open>a = b\<close> show ?thesis
  1.1264 +        using alg_mult_eq_count_roots assms in_carrier UP.nat_pow_Suc2
  1.1265 +              alg_multE(2)[OF assms(1) _ not_zero]
  1.1266 +        by auto
  1.1267 +    next
  1.1268 +      case False
  1.1269 +      have "p pdivides ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> p)"
  1.1270 +        using dividesI[OF in_carrier] UP.m_comm in_carrier assms unfolding pdivides_def by auto
  1.1271 +      thus ?thesis
  1.1272 +        using False pdivides_imp_roots_incl assms in_carrier not_zero
  1.1273 +        by (simp add: subseteq_mset_def)
  1.1274 +    qed
  1.1275 +  qed
  1.1276 +qed
  1.1277 +
  1.1278 +lemma (in domain) not_empty_rootsE[elim]:
  1.1279 +  assumes "p \<in> carrier (poly_ring R)" and "roots p \<noteq> {#}"
  1.1280 +    and "\<And>a. \<lbrakk> a \<in> carrier R; a \<in># roots p;
  1.1281 +               [ \<one>, \<ominus> a ] \<in> carrier (poly_ring R); [ \<one>, \<ominus> a ] pdivides p \<rbrakk> \<Longrightarrow> P"
  1.1282 +  shows P
  1.1283 +proof -
  1.1284 +  from \<open>roots p \<noteq> {#}\<close> obtain a where "a \<in># roots p"
  1.1285 +    by blast
  1.1286 +  with \<open>p \<in> carrier (poly_ring R)\<close> have "[ \<one>, \<ominus> a ] pdivides p"
  1.1287 +    and "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)" and "a \<in> carrier R"
  1.1288 +    using is_root_imp_pdivides[of p] roots_mem_iff_is_root[of p] is_root_def[of p a]
  1.1289 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1290 +  with \<open>a \<in># roots p\<close> show ?thesis
  1.1291 +    using assms(3)[of a] by auto
  1.1292 +qed
  1.1293 +
  1.1294 +(* REPLACE th following lemmas on Divisibility.thy ============= *)
  1.1295 +(* the only difference is the locale                             *)
  1.1296 +lemma (in monoid) mult_cong_r:
  1.1297 +  assumes "b \<sim> b'" "a \<in> carrier G"  "b \<in> carrier G"  "b' \<in> carrier G"
  1.1298 +  shows "a \<otimes> b \<sim> a \<otimes> b'"
  1.1299 +  by (meson assms associated_def divides_mult_lI)
  1.1300 +
  1.1301 +lemma (in comm_monoid) mult_cong_l:
  1.1302 +  assumes "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"  "b \<in> carrier G"
  1.1303 +  shows "a \<otimes> b \<sim> a' \<otimes> b"
  1.1304 +  using assms m_comm mult_cong_r by auto
  1.1305 +(* ============================================================= *)
  1.1306 +
  1.1307 +lemma (in field) associated_polynomials_imp_same_roots:
  1.1308 +  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "q \<in> carrier (poly_ring R)" "q \<noteq> []"
  1.1309 +  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots p + roots q"
  1.1310 +proof -
  1.1311 +  interpret UP: domain "poly_ring R"
  1.1312 +    using univ_poly_is_domain[OF carrier_is_subring] .
  1.1313 +  from assms show ?thesis
  1.1314 +  proof (induction "degree p" arbitrary: p rule: less_induct)
  1.1315 +    case less show ?case
  1.1316 +    proof (cases "roots p = {#}")
  1.1317 +      case True thus ?thesis
  1.1318 +        using no_roots_imp_same_roots[of p q] less by simp
  1.1319 +    next
  1.1320 +      case False with \<open>p \<in> carrier (poly_ring R)\<close>
  1.1321 +      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and pdiv: "[ \<one>, \<ominus> a ] pdivides p"
  1.1322 +          and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  1.1323 +        by blast
  1.1324 +      show ?thesis
  1.1325 +      proof (cases "degree p = 1")
  1.1326 +        case True with \<open>p \<in> carrier (poly_ring R)\<close>
  1.1327 +        obtain b c where p: "p = [ b, c ]" and b: "b \<in> carrier R" "b \<noteq> \<zero>" and c: "c \<in> carrier R"
  1.1328 +          by auto
  1.1329 +        with \<open>a \<in># roots p\<close> have roots: "roots p = {# a #}" and a: "\<ominus> a = inv b \<otimes> c" "a \<in> carrier R"
  1.1330 +          and lead: "lead_coeff p = b" and const: "const_term p = c"
  1.1331 +          using degree_one_imp_singleton_roots[of p] less(2) field_Units
  1.1332 +          unfolding const_term_def by auto
  1.1333 +        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)"
  1.1334 +          using UP.mult_cong_l[OF degree_one_associatedI[OF carrier_is_subfield _ True]] less(2,4)
  1.1335 +          by (auto simp add: a lead const)
  1.1336 +        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots ([ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q)"
  1.1337 +          using associated_polynomials_imp_same_roots in_carrier less(2,4) unfolding a by simp
  1.1338 +        thus ?thesis
  1.1339 +          unfolding poly_mult_degree_one_monic_imp_same_roots[OF a(2) less(4,5)] roots by simp
  1.1340 +      next
  1.1341 +        case False
  1.1342 +        from \<open>[ \<one>, \<ominus> a ] pdivides p\<close>
  1.1343 +        obtain r where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r" and r: "r \<in> carrier (poly_ring R)"
  1.1344 +          unfolding pdivides_def by auto
  1.1345 +        with \<open>p \<noteq> []\<close> have not_zero: "r \<noteq> []"
  1.1346 +          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff by auto
  1.1347 +        with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> r\<close> have deg: "degree p = Suc (degree r)"
  1.1348 +          using poly_mult_degree_eq[OF carrier_is_subring, of _ r] in_carrier r
  1.1349 +          unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  1.1350 +        with \<open>r \<noteq> []\<close> and \<open>q \<noteq> []\<close> have "r \<otimes>\<^bsub>poly_ring R\<^esub> q \<noteq> []"
  1.1351 +          using in_carrier univ_poly_zero[of R "carrier R"] UP.integral less(4) r by auto
  1.1352 +        hence "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = add_mset a (roots (r \<otimes>\<^bsub>poly_ring R\<^esub> q))"
  1.1353 +          using poly_mult_degree_one_monic_imp_same_roots[OF a UP.m_closed[OF r less(4)]]
  1.1354 +                UP.m_assoc[OF in_carrier r less(4)] p by auto
  1.1355 +        also have " ... = add_mset a (roots r + roots q)"
  1.1356 +          using less(1)[OF _ r not_zero less(4-5)] deg by simp
  1.1357 +        also have " ... = (add_mset a (roots r)) + roots q"
  1.1358 +          by simp
  1.1359 +        also have " ... = roots p + roots q"
  1.1360 +          using poly_mult_degree_one_monic_imp_same_roots[OF a r not_zero] p by simp
  1.1361 +        finally show ?thesis .
  1.1362 +      qed
  1.1363 +    qed
  1.1364 +  qed
  1.1365 +qed
  1.1366 +
  1.1367 +lemma (in field) size_roots_le_degree:
  1.1368 +  assumes "p \<in> carrier (poly_ring R)" shows "size (roots p) \<le> degree p"
  1.1369 +  using assms
  1.1370 +proof (induction "degree p" arbitrary: p rule: less_induct)
  1.1371 +  case less show ?case
  1.1372 +  proof (cases "roots p = {#}", simp)
  1.1373 +    interpret UP: domain "poly_ring R"
  1.1374 +      using univ_poly_is_domain[OF carrier_is_subring] .
  1.1375 +
  1.1376 +    case False with \<open>p \<in> carrier (poly_ring R)\<close>
  1.1377 +    obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
  1.1378 +      and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  1.1379 +      by blast
  1.1380 +    then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
  1.1381 +      unfolding pdivides_def by auto
  1.1382 +    with \<open>a \<in># roots p\<close> have "p \<noteq> []"
  1.1383 +      using degree_zero_imp_empty_roots[OF less(2)] by auto
  1.1384 +    hence not_zero: "q \<noteq> []"
  1.1385 +      using in_carrier univ_poly_zero[of R "carrier R"] UP.integral_iff p by auto
  1.1386 +    hence "degree p = Suc (degree q)"
  1.1387 +      using poly_mult_degree_eq[OF carrier_is_subring, of _ q] in_carrier p q
  1.1388 +      unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  1.1389 +    with \<open>q \<noteq> []\<close> show ?thesis
  1.1390 +      using poly_mult_degree_one_monic_imp_same_roots[OF a q] p less(1)[OF _ q]
  1.1391 +      by (metis Suc_le_mono lessI size_add_mset)
  1.1392 +  qed
  1.1393 +qed
  1.1394 +
  1.1395 +(* MOVE to Divisibility.thy ======== *)
  1.1396 +lemma divides_irreducible_condition:
  1.1397 +  assumes "irreducible G r" and "a \<in> carrier G"
  1.1398 +  shows "a divides\<^bsub>G\<^esub> r \<Longrightarrow> a \<in> Units G \<or> a \<sim>\<^bsub>G\<^esub> r"
  1.1399 +  using assms unfolding irreducible_def properfactor_def associated_def
  1.1400 +  by (cases "r divides\<^bsub>G\<^esub> a", auto)
  1.1401 +
  1.1402 +(* MOVE to Polynomial_Divisibility.thy ======== *)
  1.1403 +lemma (in ring) divides_pirreducible_condition:
  1.1404 +  assumes "pirreducible K q" and "p \<in> carrier (K[X])"
  1.1405 +  shows "p divides\<^bsub>K[X]\<^esub> q \<Longrightarrow> p \<in> Units (K[X]) \<or> p \<sim>\<^bsub>K[X]\<^esub> q"
  1.1406 +  using divides_irreducible_condition[of "K[X]" q p] assms
  1.1407 +  unfolding ring_irreducible_def by auto
  1.1408 +
  1.1409 +lemma (in domain) pirreducible_roots:
  1.1410 +  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
  1.1411 +  shows "roots p = {#}"
  1.1412 +proof (rule ccontr)
  1.1413 +  assume "roots p \<noteq> {#}" with \<open>p \<in> carrier (poly_ring R)\<close>
  1.1414 +  obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
  1.1415 +    and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  1.1416 +    by blast
  1.1417 +  hence "[ \<one>, \<ominus> a ] \<sim>\<^bsub>poly_ring R\<^esub> p"
  1.1418 +    using divides_pirreducible_condition[OF assms(2) in_carrier]
  1.1419 +          univ_poly_units_incl[OF carrier_is_subring]
  1.1420 +    unfolding pdivides_def by auto
  1.1421 +  hence "degree p = 1"
  1.1422 +    using associated_polynomials_imp_same_length[OF carrier_is_subring in_carrier assms(1)] by auto
  1.1423 +  with \<open>degree p \<noteq> 1\<close> show False ..
  1.1424 +qed
  1.1425 +
  1.1426 +lemma (in field) pirreducible_imp_not_splitted:
  1.1427 +  assumes "p \<in> carrier (poly_ring R)" and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
  1.1428 +  shows "\<not> splitted p"
  1.1429 +  using pirreducible_roots[of p] pirreducible_degree[OF carrier_is_subfield, of p] assms
  1.1430 +  by (simp add: splitted_def)
  1.1431 +
  1.1432 +lemma (in field)
  1.1433 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)"
  1.1434 +    and "pirreducible (carrier R) p" and "degree p \<noteq> 1"
  1.1435 +  shows "roots (p \<otimes>\<^bsub>poly_ring R\<^esub> q) = roots q"
  1.1436 +  using no_roots_imp_same_roots[of p q] pirreducible_roots[of p] assms
  1.1437 +  unfolding ring_irreducible_def univ_poly_zero by auto
  1.1438 +
  1.1439 +lemma (in field) trivial_factors_imp_splitted:
  1.1440 +  assumes "p \<in> carrier (poly_ring R)"
  1.1441 +    and "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q \<le> 1"
  1.1442 +  shows "splitted p"
  1.1443 +  using assms
  1.1444 +proof (induction "degree p" arbitrary: p rule: less_induct)
  1.1445 +  interpret UP: principal_domain "poly_ring R"
  1.1446 +    using univ_poly_is_principal[OF carrier_is_subfield] .
  1.1447 +  case less show ?case
  1.1448 +  proof (cases "degree p = 0", simp add: degree_zero_imp_splitted[OF less(2)])
  1.1449 +    case False show ?thesis
  1.1450 +    proof (cases "roots p = {#}")
  1.1451 +      case True
  1.1452 +      from \<open>degree p \<noteq> 0\<close> have "p \<notin> Units (poly_ring R)" and "p \<in> carrier (poly_ring R) - { [] }"
  1.1453 +        using univ_poly_units'[OF carrier_is_subfield, of p] less(2) by auto
  1.1454 +      then obtain q where "q \<in> carrier (poly_ring R)" "pirreducible (carrier R) q" and "q pdivides p"
  1.1455 +        using UP.exists_irreducible_divisor[of p] unfolding univ_poly_zero pdivides_def by auto
  1.1456 +      with \<open>degree p \<noteq> 0\<close> have "roots p \<noteq> {#}"
  1.1457 +        using degree_one_imp_singleton_roots[OF _ , of q] less(3)[of q]
  1.1458 +              pdivides_imp_roots_incl[OF _ less(2), of q]
  1.1459 +              pirreducible_degree[OF carrier_is_subfield, of q]
  1.1460 +        by force
  1.1461 +      from \<open>roots p = {#}\<close> and \<open>roots p \<noteq> {#}\<close> have False
  1.1462 +        by simp
  1.1463 +      thus ?thesis ..
  1.1464 +    next
  1.1465 +      case False with \<open>p \<in> carrier (poly_ring R)\<close>
  1.1466 +      obtain a where a: "a \<in> carrier R" and "a \<in># roots p" and "[ \<one>, \<ominus> a ] pdivides p"
  1.1467 +        and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  1.1468 +        by blast
  1.1469 +      then obtain q where p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q" and q: "q \<in> carrier (poly_ring R)"
  1.1470 +        unfolding pdivides_def by blast
  1.1471 +      with \<open>degree p \<noteq> 0\<close> have "p \<noteq> []"
  1.1472 +        by auto
  1.1473 +      with \<open>p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q\<close> have "q \<noteq> []"
  1.1474 +        using in_carrier q unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
  1.1475 +      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)"
  1.1476 +        using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q
  1.1477 +        unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  1.1478 +      moreover have "q pdivides p"
  1.1479 +        using p dividesI[OF in_carrier] UP.m_comm[OF in_carrier q] by (auto simp add: pdivides_def)
  1.1480 +      hence "degree r = 1" if "r \<in> carrier (poly_ring R)" and "pirreducible (carrier R) r"
  1.1481 +        and "r pdivides q" for r
  1.1482 +        using less(3)[OF that(1-2)] UP.divides_trans[OF _ _ that(1), of q p] that(3)
  1.1483 +              pirreducible_degree[OF carrier_is_subfield that(1-2)]
  1.1484 +        by (auto simp add: pdivides_def)
  1.1485 +      ultimately have "splitted q"
  1.1486 +        using less(1)[OF _ q] by auto
  1.1487 +      with \<open>degree p = Suc (degree q)\<close> and \<open>q \<noteq> []\<close> show ?thesis
  1.1488 +        using poly_mult_degree_one_monic_imp_same_roots[OF a q]
  1.1489 +        unfolding sym[OF p] splitted_def
  1.1490 +        by simp
  1.1491 +    qed
  1.1492 +  qed
  1.1493 +qed
  1.1494 +
  1.1495 +lemma (in field) pdivides_imp_splitted:
  1.1496 +  assumes "p \<in> carrier (poly_ring R)" and "q \<in> carrier (poly_ring R)" "q \<noteq> []" and "splitted q"
  1.1497 +  shows "p pdivides q \<Longrightarrow> splitted p"
  1.1498 +proof (cases "p = []")
  1.1499 +  case True thus ?thesis
  1.1500 +    using degree_zero_imp_splitted[OF assms(1)] by simp
  1.1501 +next
  1.1502 +  interpret UP: principal_domain "poly_ring R"
  1.1503 +    using univ_poly_is_principal[OF carrier_is_subfield] .
  1.1504 +
  1.1505 +  case False
  1.1506 +  assume "p pdivides q"
  1.1507 +  then obtain b where b: "b \<in> carrier (poly_ring R)" and q: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
  1.1508 +    unfolding pdivides_def by auto
  1.1509 +  with \<open>q \<noteq> []\<close> have "p \<noteq> []" and "b \<noteq> []"
  1.1510 +    using assms UP.integral_iff[of p b] unfolding sym[OF univ_poly_zero[of R "carrier R"]] by auto
  1.1511 +  hence "degree p + degree b = size (roots p) + size (roots b)"
  1.1512 +    using associated_polynomials_imp_same_roots[of p b] assms b q splitted_def
  1.1513 +          poly_mult_degree_eq[OF carrier_is_subring,of p b]
  1.1514 +    unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]]
  1.1515 +    by auto
  1.1516 +  moreover have "size (roots p) \<le> degree p" and "size (roots b) \<le> degree b"
  1.1517 +    using size_roots_le_degree assms(1) b by auto
  1.1518 +  ultimately show ?thesis
  1.1519 +    unfolding splitted_def by linarith
  1.1520 +qed
  1.1521 +
  1.1522 +lemma (in field) splitted_imp_trivial_factors:
  1.1523 +  assumes "p \<in> carrier (poly_ring R)" "p \<noteq> []" and "splitted p"
  1.1524 +  shows "\<And>q. \<lbrakk> q \<in> carrier (poly_ring R); pirreducible (carrier R) q; q pdivides p \<rbrakk> \<Longrightarrow> degree q = 1"
  1.1525 +  using pdivides_imp_splitted[OF _ assms] pirreducible_imp_not_splitted
  1.1526 +  by auto
  1.1527 +
  1.1528  lemma (in field) exists_root:
  1.1529    assumes "M \<in> extensions" and "\<And>L. \<lbrakk> L \<in> extensions; M \<lesssim> L \<rbrakk> \<Longrightarrow> law_restrict L = law_restrict M"
  1.1530 -    and "P \<in> carrier (poly_ring R)" and "degree P > 0"
  1.1531 -  shows "\<exists>x \<in> carrier M. (ring.eval M) (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>"
  1.1532 +    and "P \<in> carrier (poly_ring R)"
  1.1533 +  shows "(ring.splitted M) (\<sigma> P)"
  1.1534  proof (rule ccontr)
  1.1535    from \<open>M \<in> extensions\<close> interpret M: field M + Hom: ring_hom_ring R M "indexed_const"
  1.1536      using ring_hom_ringI2[OF ring_axioms field.is_ring] unfolding extensions_def by auto
  1.1537    interpret UP: principal_domain "poly_ring M"
  1.1538      using M.univ_poly_is_principal[OF M.carrier_is_subfield] .
  1.1539  
  1.1540 -  assume no_roots: "\<not> (\<exists>x \<in> carrier M. M.eval (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>)"
  1.1541 +  assume not_splitted: "\<not> (ring.splitted M) (\<sigma> P)"
  1.1542    have "(\<sigma> P) \<in> carrier (poly_ring M)"
  1.1543      using polynomial_hom[OF Hom.homh field_axioms M.field_axioms assms(3)] unfolding \<sigma>_def by simp
  1.1544 -  moreover have "(\<sigma> P) \<notin> Units (poly_ring M)" and "(\<sigma> P) \<noteq> \<zero>\<^bsub>poly_ring M\<^esub>"
  1.1545 -    using assms(4) unfolding M.univ_poly_carrier_units \<sigma>_def univ_poly_zero by auto
  1.1546 -  ultimately obtain Q
  1.1547 +  then obtain Q
  1.1548      where Q: "Q \<in> carrier (poly_ring M)" "pirreducible\<^bsub>M\<^esub> (carrier M) Q" "Q pdivides\<^bsub>M\<^esub> (\<sigma> P)"
  1.1549 -    using UP.exists_irreducible_divisor[of "\<sigma> P"] unfolding pdivides_def by blast
  1.1550 +      and degree_gt: "degree Q > 1"
  1.1551 +    using M.trivial_factors_imp_splitted[of "\<sigma> P"] not_splitted by force
  1.1552 +
  1.1553 +  from \<open>(\<sigma> P) \<in> carrier (poly_ring M)\<close> have "(\<sigma> P) \<noteq> []"
  1.1554 +    using M.degree_zero_imp_splitted[of "\<sigma> P"] not_splitted unfolding \<sigma>_def by auto
  1.1555  
  1.1556 -  have hyps:
  1.1557 +  have "\<exists>i. \<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
  1.1558 +  proof (rule ccontr)
  1.1559 +    assume "\<nexists>i. \<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
  1.1560 +    then have "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier M" and "(ring.eval M) (\<sigma> P) \<X>\<^bsub>(P, i)\<^esub> = \<zero>\<^bsub>M\<^esub>" for i
  1.1561 +      using assms(1,3) unfolding extensions_def by blast+
  1.1562 +    with \<open>(\<sigma> P) \<noteq> []\<close> have "((\<lambda>i :: nat. \<X>\<^bsub>(P, i)\<^esub>) ` UNIV) \<subseteq> { a. (ring.is_root M) (\<sigma> P) a }"
  1.1563 +      unfolding M.is_root_def by auto
  1.1564 +    moreover have "inj (\<lambda>i :: nat. \<X>\<^bsub>(P, i)\<^esub>)"
  1.1565 +      unfolding indexed_var_def indexed_const_def indexed_pmult_def inj_def
  1.1566 +      by (metis (no_types, lifting) add_mset_eq_singleton_iff diff_single_eq_union
  1.1567 +                                    multi_member_last prod.inject zero_not_one)
  1.1568 +    hence "infinite ((\<lambda>i :: nat. \<X>\<^bsub>(P, i)\<^esub>) ` UNIV)"
  1.1569 +      unfolding infinite_iff_countable_subset by auto
  1.1570 +    ultimately have "infinite { a. (ring.is_root M) (\<sigma> P) a }"
  1.1571 +      using finite_subset by auto
  1.1572 +    with \<open>(\<sigma> P) \<in> carrier (poly_ring M)\<close> show False
  1.1573 +      using M.finite_number_of_roots by simp
  1.1574 +  qed
  1.1575 +  then obtain i :: nat where "\<forall>\<P> \<in> carrier M. index_free \<P> (P, i)"
  1.1576 +    by blast
  1.1577 +
  1.1578 +  then have hyps:
  1.1579      \<comment> \<open>i\<close>   "field M"
  1.1580      \<comment> \<open>ii\<close>  "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> carrier_coeff \<P>"
  1.1581 -    \<comment> \<open>iii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> index_free \<P> P"
  1.1582 +    \<comment> \<open>iii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> index_free \<P> (P, i)"
  1.1583      \<comment> \<open>iv\<close>  "\<zero>\<^bsub>M\<^esub> = indexed_const \<zero>"
  1.1584 -    using assms(1,3) no_roots unfolding extensions_def by auto
  1.1585 -  have degree_gt: "degree Q > 1"
  1.1586 -  proof (rule ccontr)
  1.1587 -    assume "\<not> degree Q > 1" hence "degree Q = 1"
  1.1588 -      using M.pirreducible_degree[OF M.carrier_is_subfield Q(1-2)] by simp
  1.1589 -    then obtain x where "x \<in> carrier M" and "M.eval Q x = \<zero>\<^bsub>M\<^esub>"
  1.1590 -      using M.degree_one_root[OF M.carrier_is_subfield Q(1)] M.add.inv_closed by blast  
  1.1591 -    hence "M.eval (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>"
  1.1592 -      using M.pdivides_imp_root_sharing[OF Q(1,3)] by simp
  1.1593 -    with \<open>x \<in> carrier M\<close> show False
  1.1594 -      using no_roots by simp
  1.1595 -  qed
  1.1596 +    using assms(1,3) unfolding extensions_def by auto
  1.1597  
  1.1598 -  define image_poly where "image_poly = image_ring (eval_pmod M P Q) (poly_ring M)"
  1.1599 +  define image_poly where "image_poly = image_ring (eval_pmod M (P, i) Q) (poly_ring M)"
  1.1600    with \<open>degree Q > 1\<close> have "M \<lesssim> image_poly"
  1.1601      using image_poly_iso_incl[OF hyps Q(1)] by auto
  1.1602    moreover have is_field: "field image_poly"
  1.1603 @@ -530,7 +1745,7 @@
  1.1604    moreover have "image_poly \<in> extensions"
  1.1605    proof (auto simp add: extensions_def is_field)
  1.1606      fix \<P> assume "\<P> \<in> carrier image_poly"
  1.1607 -    then obtain R where \<P>: "\<P> = eval_pmod M P Q R" and "R \<in> carrier (poly_ring M)"
  1.1608 +    then obtain R where \<P>: "\<P> = eval_pmod M (P, i) Q R" and "R \<in> carrier (poly_ring M)"
  1.1609        unfolding image_poly_def image_ring_carrier by auto
  1.1610      hence "M.pmod R Q \<in> carrier (poly_ring M)"
  1.1611        using M.long_division_closed(2)[OF M.carrier_is_subfield _ Q(1)] by simp
  1.1612 @@ -545,32 +1760,32 @@
  1.1613      from \<open>M \<lesssim> image_poly\<close> interpret Id: ring_hom_ring M image_poly id
  1.1614        using iso_inclE[OF M.ring_axioms field.is_ring[OF is_field]] by simp
  1.1615  
  1.1616 -    fix \<P> S
  1.1617 -    assume A: "\<P> \<in> carrier image_poly" "\<not> index_free \<P> S" "S \<in> carrier (poly_ring R)"
  1.1618 -    have "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly \<and> Id.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
  1.1619 +    fix \<P> S j
  1.1620 +    assume A: "\<P> \<in> carrier image_poly" "\<not> index_free \<P> (S, j)" "S \<in> carrier (poly_ring R)"
  1.1621 +    have "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier image_poly \<and> Id.eval (\<sigma> S) \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
  1.1622      proof (cases)
  1.1623 -      assume "P \<noteq> S"
  1.1624 -      then obtain Q' where "Q' \<in> carrier M" and "\<not> index_free Q' S"
  1.1625 +      assume "(P, i) \<noteq> (S, j)"
  1.1626 +      then obtain Q' where "Q' \<in> carrier M" and "\<not> index_free Q' (S, j)"
  1.1627          using A(1) image_poly_index_free[OF hyps Q(1) _ A(2)] unfolding image_poly_def by auto
  1.1628 -      hence "\<X>\<^bsub>S\<^esub> \<in> carrier M" and "M.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>M\<^esub>"
  1.1629 +      hence "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier M" and "M.eval (\<sigma> S) \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>M\<^esub>"
  1.1630          using assms(1) A(3) unfolding extensions_def by auto
  1.1631        moreover have "\<sigma> S \<in> carrier (poly_ring M)"
  1.1632          using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \<sigma>_def .
  1.1633        ultimately show ?thesis
  1.1634          using Id.eval_hom[OF M.carrier_is_subring] Id.hom_closed Id.hom_zero by auto
  1.1635      next
  1.1636 -      assume "\<not> P \<noteq> S" hence S: "P = S"
  1.1637 +      assume "\<not> (P, i) \<noteq> (S, j)" hence S: "(P, i) = (S, j)"
  1.1638          by simp
  1.1639        have poly_hom: "R \<in> carrier (poly_ring image_poly)" if "R \<in> carrier (poly_ring M)" for R
  1.1640          using polynomial_hom[OF Id.homh M.field_axioms is_field that] by simp
  1.1641 -      have "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly"
  1.1642 +      have "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier image_poly"
  1.1643          using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def S by simp
  1.1644 -      moreover have "Id.eval Q \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
  1.1645 +      moreover have "Id.eval Q \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
  1.1646          using image_poly_eval_indexed_var[OF hyps Hom.homh Q(1) degree_gt Q(2)] unfolding image_poly_def S by simp
  1.1647        moreover have "Q pdivides\<^bsub>image_poly\<^esub> (\<sigma> S)"
  1.1648        proof -
  1.1649          obtain R where R: "R \<in> carrier (poly_ring M)" "\<sigma> S = Q \<otimes>\<^bsub>poly_ring M\<^esub> R"
  1.1650 -          using Q(3) unfolding S pdivides_def by auto
  1.1651 +          using Q(3) S unfolding pdivides_def by auto
  1.1652          moreover have "set Q \<subseteq> carrier M" and "set R \<subseteq> carrier M"
  1.1653            using Q(1) R(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1654          ultimately have "Id.normalize (\<sigma> S) = Q \<otimes>\<^bsub>poly_ring image_poly\<^esub> R"
  1.1655 @@ -590,23 +1805,22 @@
  1.1656        ultimately show ?thesis
  1.1657          using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF is_field], of Q] by auto
  1.1658      qed
  1.1659 -    thus "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly" and "Id.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
  1.1660 +    thus "\<X>\<^bsub>(S, j)\<^esub> \<in> carrier image_poly" and "Id.eval (\<sigma> S) \<X>\<^bsub>(S, j)\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
  1.1661        by auto
  1.1662    qed
  1.1663    ultimately have "law_restrict M = law_restrict image_poly"
  1.1664      using assms(2) by simp
  1.1665    hence "carrier M = carrier image_poly"
  1.1666      unfolding law_restrict_def by (simp add:ring.defs)
  1.1667 -  moreover have "\<X>\<^bsub>P\<^esub> \<in> carrier image_poly"
  1.1668 +  moreover have "\<X>\<^bsub>(P, i)\<^esub> \<in> carrier image_poly"
  1.1669      using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def by simp
  1.1670 -  moreover have "\<X>\<^bsub>P\<^esub> \<notin> carrier M"
  1.1671 -    using indexed_var_not_index_free[of P] hyps(3) by blast
  1.1672 +  moreover have "\<X>\<^bsub>(P, i)\<^esub> \<notin> carrier M"
  1.1673 +    using indexed_var_not_index_free[of "(P, i)"] hyps(3) by blast
  1.1674    ultimately show False by simp
  1.1675  qed
  1.1676  
  1.1677  lemma (in field) exists_extension_with_roots:
  1.1678 -  shows "\<exists>L \<in> extensions. \<forall>P \<in> carrier (poly_ring R).
  1.1679 -    degree P > 0 \<longrightarrow> (\<exists>x \<in> carrier L. (ring.eval L) (\<sigma> P) x = \<zero>\<^bsub>L\<^esub>)"
  1.1680 +  shows "\<exists>L \<in> extensions. \<forall>P \<in> carrier (poly_ring R). (ring.splitted L) (\<sigma> P)"
  1.1681  proof -
  1.1682    obtain M where "M \<in> extensions" and "\<forall>L \<in> extensions. M \<lesssim> L \<longrightarrow> law_restrict L = law_restrict M"
  1.1683      using exists_maximal_extension iso_incl_hom by blast
  1.1684 @@ -619,17 +1833,16 @@
  1.1685  
  1.1686  locale algebraic_closure = field L + subfield K L for L (structure) and K +
  1.1687    assumes algebraic_extension: "x \<in> carrier L \<Longrightarrow> (algebraic over K) x"
  1.1688 -    and roots_over_subfield: "\<lbrakk> P \<in> carrier (K[X]); degree P > 0 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier L. eval P x = \<zero>\<^bsub>L\<^esub>"
  1.1689 +    and roots_over_subfield: "P \<in> carrier (K[X]) \<Longrightarrow> splitted P"
  1.1690  
  1.1691  locale algebraically_closed = field L for L (structure) +
  1.1692 -  assumes roots_over_carrier: "\<lbrakk> P \<in> carrier (poly_ring L); degree P > 0 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier L. eval P x = \<zero>\<^bsub>L\<^esub>"
  1.1693 +  assumes roots_over_carrier: "P \<in> carrier (poly_ring L) \<Longrightarrow> splitted P"
  1.1694  
  1.1695 -definition (in field) closure :: "(('a list) multiset \<Rightarrow> 'a) ring" ("\<Omega>")
  1.1696 +definition (in field) closure :: "(('a list \<times> nat) multiset \<Rightarrow> 'a) ring" ("\<Omega>")
  1.1697    where "closure = (SOME L \<comment> \<open>such that\<close>.
  1.1698 -           \<comment> \<open>i\<close>  algebraic_closure L (indexed_const ` (carrier R)) \<and> 
  1.1699 +           \<comment> \<open>i\<close>  algebraic_closure L (indexed_const ` (carrier R)) \<and>
  1.1700             \<comment> \<open>ii\<close> indexed_const \<in> ring_hom R L)"
  1.1701  
  1.1702 -
  1.1703  lemma algebraic_hom:
  1.1704    assumes "h \<in> ring_hom R S" and "field R" and "field S" and "subfield K R" and "x \<in> carrier R"
  1.1705    shows "((ring.algebraic R) over K) x \<Longrightarrow> ((ring.algebraic S) over (h ` K)) (h x)"
  1.1706 @@ -648,12 +1861,11 @@
  1.1707  qed
  1.1708  
  1.1709  lemma (in field) exists_closure:
  1.1710 -  obtains L :: "(('a list multiset) \<Rightarrow> 'a) ring"
  1.1711 +  obtains L :: "((('a list \<times> nat) multiset) \<Rightarrow> 'a) ring"
  1.1712    where "algebraic_closure L (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R L"
  1.1713  proof -
  1.1714    obtain L where "L \<in> extensions"
  1.1715 -    and roots: "\<And>P. \<lbrakk> P \<in> carrier (poly_ring R); degree P > 0 \<rbrakk> \<Longrightarrow>
  1.1716 -                      \<exists>x \<in> carrier L. (ring.eval L) (\<sigma> P) x = \<zero>\<^bsub>L\<^esub>"
  1.1717 +    and roots: "\<And>P. P \<in> carrier (poly_ring R) \<Longrightarrow> (ring.splitted L) (\<sigma> P)"
  1.1718      using exists_extension_with_roots by auto
  1.1719  
  1.1720    let ?K = "indexed_const ` (carrier R)"
  1.1721 @@ -685,7 +1897,7 @@
  1.1722    next
  1.1723      show "?K \<subseteq> carrier ?M"
  1.1724      proof
  1.1725 -      fix x :: "('a list multiset) \<Rightarrow> 'a"
  1.1726 +      fix x :: "(('a list \<times> nat) multiset) \<Rightarrow> 'a"
  1.1727        assume "x \<in> ?K"
  1.1728        hence "x \<in> carrier L"
  1.1729          using ring_hom_memE(1)[OF ring_hom_ring.homh[OF hom]] by auto
  1.1730 @@ -700,54 +1912,126 @@
  1.1731    proof (intro algebraic_closure.intro[OF M is_subfield])
  1.1732      have "(Id.R.algebraic over ?K) x" if "x \<in> carrier ?M" for x
  1.1733        using that Id.S.algebraic_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
  1.1734 -    moreover have "\<exists>x \<in> carrier ?M. Id.R.eval P x = \<zero>\<^bsub>?M\<^esub>"
  1.1735 -      if "P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)" and "degree P > 0" for P
  1.1736 +    moreover have "Id.R.splitted P" if "P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)" for P
  1.1737      proof -
  1.1738 -      from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (?K[X]\<^bsub>L\<^esub>)"
  1.1739 -        unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] .
  1.1740 -      hence "set P \<subseteq> ?K"
  1.1741 -        unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1742 -      hence "\<exists>Q. set Q \<subseteq> carrier R \<and> P = \<sigma> Q"
  1.1743 -      proof (induct P, simp add: \<sigma>_def)
  1.1744 -        case (Cons p P)
  1.1745 -        then obtain q Q where "q \<in> carrier R" "set Q \<subseteq> carrier R" and "\<sigma> Q = P""indexed_const q = p"
  1.1746 -          unfolding \<sigma>_def by auto
  1.1747 -        hence "set (q # Q) \<subseteq> carrier R" and "\<sigma> (q # Q) = (p # P)"
  1.1748 -          unfolding \<sigma>_def by auto
  1.1749 -        thus ?case
  1.1750 -          by metis
  1.1751 -      qed
  1.1752 -      then obtain Q where "set Q \<subseteq> carrier R" and "\<sigma> Q = P"
  1.1753 -        by auto
  1.1754 -      moreover have "lead_coeff Q \<noteq> \<zero>"
  1.1755 -      proof (rule ccontr)
  1.1756 -        assume "\<not> lead_coeff Q \<noteq> \<zero>" then have "lead_coeff Q = \<zero>"
  1.1757 +      from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (poly_ring ?M)"
  1.1758 +        using Id.R.carrier_polynomial_shell[OF subfieldE(1)[OF is_subfield]] by simp
  1.1759 +      show ?thesis
  1.1760 +      proof (cases "degree P = 0")
  1.1761 +        case True with \<open>P \<in> carrier (poly_ring ?M)\<close> show ?thesis
  1.1762 +          using domain.degree_zero_imp_splitted[OF field.axioms(1)[OF M]]
  1.1763 +          by fastforce
  1.1764 +      next
  1.1765 +        case False then have "degree P > 0"
  1.1766            by simp
  1.1767 -        with \<open>\<sigma> Q = P\<close> and \<open>degree P > 0\<close> have "lead_coeff P = indexed_const \<zero>"
  1.1768 -          unfolding \<sigma>_def by (metis diff_0_eq_0 length_map less_irrefl_nat list.map_sel(1) list.size(3))
  1.1769 -        hence "lead_coeff P = \<zero>\<^bsub>L\<^esub>"
  1.1770 -          using ring_hom_zero[OF ring_hom_ring.homh ring_hom_ring.axioms(1-2)] hom by auto
  1.1771 -        with \<open>degree P > 0\<close> have "\<not> P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)"
  1.1772 +        from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (?K[X]\<^bsub>L\<^esub>)"
  1.1773 +          unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] .
  1.1774 +        hence "set P \<subseteq> ?K"
  1.1775 +          unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1776 +        hence "\<exists>Q. set Q \<subseteq> carrier R \<and> P = \<sigma> Q"
  1.1777 +        proof (induct P, simp add: \<sigma>_def)
  1.1778 +          case (Cons p P)
  1.1779 +          then obtain q Q where "q \<in> carrier R" "set Q \<subseteq> carrier R"
  1.1780 +            and "\<sigma> Q = P" "indexed_const q = p"
  1.1781 +            unfolding \<sigma>_def by auto
  1.1782 +          hence "set (q # Q) \<subseteq> carrier R" and "\<sigma> (q # Q) = (p # P)"
  1.1783 +            unfolding \<sigma>_def by auto
  1.1784 +          thus ?case
  1.1785 +            by metis
  1.1786 +        qed
  1.1787 +        then obtain Q where "set Q \<subseteq> carrier R" and "\<sigma> Q = P"
  1.1788 +          by auto
  1.1789 +        moreover have "lead_coeff Q \<noteq> \<zero>"
  1.1790 +        proof (rule ccontr)
  1.1791 +          assume "\<not> lead_coeff Q \<noteq> \<zero>" then have "lead_coeff Q = \<zero>"
  1.1792 +            by simp
  1.1793 +          with \<open>\<sigma> Q = P\<close> and \<open>degree P > 0\<close> have "lead_coeff P = indexed_const \<zero>"
  1.1794 +            unfolding \<sigma>_def by (metis diff_0_eq_0 length_map less_irrefl_nat list.map_sel(1) list.size(3))
  1.1795 +          hence "lead_coeff P = \<zero>\<^bsub>L\<^esub>"
  1.1796 +            using ring_hom_zero[OF ring_hom_ring.homh ring_hom_ring.axioms(1-2)] hom by auto
  1.1797 +          with \<open>degree P > 0\<close> have "\<not> P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)"
  1.1798 +            unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1799 +          with \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> show False
  1.1800 +            by simp
  1.1801 +        qed
  1.1802 +        ultimately have "Q \<in> carrier (poly_ring R)"
  1.1803            unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1804 -        with \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> show False
  1.1805 -          by simp
  1.1806 +        with \<open>\<sigma> Q = P\<close> have "Id.S.splitted P"
  1.1807 +          using roots[of Q] by simp
  1.1808 +
  1.1809 +        from \<open>P \<in> carrier (poly_ring ?M)\<close> show ?thesis
  1.1810 +        proof (rule field.trivial_factors_imp_splitted[OF M])
  1.1811 +          fix R
  1.1812 +          assume R: "R \<in> carrier (poly_ring ?M)" "pirreducible\<^bsub>?M\<^esub> (carrier ?M) R" and "R pdivides\<^bsub>?M\<^esub> P"
  1.1813 +
  1.1814 +          from \<open>P \<in> carrier (poly_ring ?M)\<close> and \<open>R \<in> carrier (poly_ring ?M)\<close>
  1.1815 +          have "P \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)" and "R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)"
  1.1816 +            unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by auto
  1.1817 +          hence in_carrier: "P \<in> carrier (poly_ring L)" "R \<in> carrier (poly_ring L)"
  1.1818 +            using Id.S.carrier_polynomial_shell[OF subfieldE(1)[OF set_of_algs]] by auto
  1.1819 +
  1.1820 +          from \<open>R pdivides\<^bsub>?M\<^esub> P\<close> have "R divides\<^bsub>((?set_of_algs)[X]\<^bsub>L\<^esub>)\<^esub> P"
  1.1821 +            unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]]
  1.1822 +            by simp
  1.1823 +          with \<open>P \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close> and \<open>R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
  1.1824 +          have "R pdivides\<^bsub>L\<^esub> P"
  1.1825 +            using domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs, of R P] by simp
  1.1826 +          with \<open>Id.S.splitted P\<close> and \<open>degree P \<noteq> 0\<close> have "Id.S.splitted R"
  1.1827 +            using field.pdivides_imp_splitted[OF L in_carrier(2,1)] by fastforce
  1.1828 +          show "degree R \<le> 1"
  1.1829 +          proof (cases "Id.S.roots R = {#}")
  1.1830 +            case True with \<open>Id.S.splitted R\<close> show ?thesis
  1.1831 +              unfolding Id.S.splitted_def by simp
  1.1832 +          next
  1.1833 +            case False with \<open>R \<in> carrier (poly_ring L)\<close>
  1.1834 +            obtain a where "a \<in> carrier L" and "a \<in># Id.S.roots R"
  1.1835 +              and "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring L)" and pdiv: "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] pdivides\<^bsub>L\<^esub> R"
  1.1836 +              using domain.not_empty_rootsE[OF field.axioms(1)[OF L], of R] by blast
  1.1837 +
  1.1838 +            from \<open>P \<in> carrier (?K[X]\<^bsub>L\<^esub>)\<close>
  1.1839 +            have "(Id.S.algebraic over ?K) a"
  1.1840 +            proof (rule Id.S.algebraicI)
  1.1841 +              from \<open>degree P \<noteq> 0\<close> show "P \<noteq> []"
  1.1842 +                by auto
  1.1843 +            next
  1.1844 +              from \<open>a \<in># Id.S.roots R\<close> and \<open>R \<in> carrier (poly_ring L)\<close>
  1.1845 +              have "Id.S.eval R a = \<zero>\<^bsub>L\<^esub>"
  1.1846 +                using domain.roots_mem_iff_is_root[OF field.axioms(1)[OF L]]
  1.1847 +                unfolding Id.S.is_root_def by auto
  1.1848 +              with \<open>R pdivides\<^bsub>L\<^esub> P\<close> and \<open>a \<in> carrier L\<close> show "Id.S.eval P a = \<zero>\<^bsub>L\<^esub>"
  1.1849 +                using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF L] in_carrier(2)] by simp
  1.1850 +            qed
  1.1851 +            with \<open>a \<in> carrier L\<close> have "a \<in> ?set_of_algs"
  1.1852 +              by simp
  1.1853 +            hence "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)"
  1.1854 +              using subringE(3,5)[of ?set_of_algs L] subfieldE(1,6)[OF set_of_algs]
  1.1855 +              unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  1.1856 +            hence "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier (poly_ring ?M)"
  1.1857 +              unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
  1.1858 +
  1.1859 +            from \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
  1.1860 +             and \<open>R \<in> carrier ((?set_of_algs)[X]\<^bsub>L\<^esub>)\<close>
  1.1861 +            have "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>(?set_of_algs)[X]\<^bsub>L\<^esub>\<^esub> R"
  1.1862 +              using pdiv domain.pdivides_iff_shell[OF field.axioms(1)[OF L] set_of_algs] by simp
  1.1863 +            hence "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>poly_ring ?M\<^esub> R"
  1.1864 +              unfolding pdivides_def Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]]
  1.1865 +              by simp
  1.1866 +
  1.1867 +            have "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<notin> Units (poly_ring ?M)"
  1.1868 +              using Id.R.univ_poly_units[OF field.carrier_is_subfield[OF M]] by force
  1.1869 +            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>
  1.1870 +             and \<open>[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] divides\<^bsub>poly_ring ?M\<^esub> R\<close>
  1.1871 +            have "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ] \<sim>\<^bsub>poly_ring ?M\<^esub> R"
  1.1872 +              using Id.R.divides_pirreducible_condition[OF R(2)] by auto
  1.1873 +            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>
  1.1874 +            have "degree R = 1"
  1.1875 +              using domain.associated_polynomials_imp_same_length[OF field.axioms(1)[OF M]
  1.1876 +                    Id.R.carrier_is_subring, of "[ \<one>\<^bsub>L\<^esub>, \<ominus>\<^bsub>L\<^esub> a ]" R] by force
  1.1877 +            thus ?thesis
  1.1878 +              by simp
  1.1879 +          qed
  1.1880 +        qed
  1.1881        qed
  1.1882 -      ultimately have "Q \<in> carrier (poly_ring R)"
  1.1883 -        unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1884 -      moreover from \<open>degree P > 0\<close> and \<open>\<sigma> Q = P\<close> have "degree Q > 0"
  1.1885 -        unfolding \<sigma>_def by auto
  1.1886 -      ultimately obtain x where "x \<in> carrier L" and "Id.S.eval P x = \<zero>\<^bsub>L\<^esub>"
  1.1887 -        using roots[of Q] unfolding \<open>\<sigma> Q = P\<close> by auto
  1.1888 -      hence "Id.R.eval P x = \<zero>\<^bsub>?M\<^esub>"
  1.1889 -        unfolding Id.S.eval_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
  1.1890 -      moreover from \<open>degree P > 0\<close> have "P \<noteq> []"
  1.1891 -        by auto
  1.1892 -      with \<open>P \<in> carrier (?K[X]\<^bsub>L\<^esub>)\<close> and \<open>Id.S.eval P x = \<zero>\<^bsub>L\<^esub>\<close> have "(Id.S.algebraic over ?K) x"
  1.1893 -        using Id.S.non_trivial_ker_imp_algebraic[of ?K x] unfolding a_kernel_def' by auto
  1.1894 -      with \<open>x \<in> carrier L\<close> have "x \<in> carrier ?M"
  1.1895 -        by auto
  1.1896 -      ultimately show ?thesis
  1.1897 -        by auto
  1.1898      qed
  1.1899      ultimately show "algebraic_closure_axioms ?M ?K"
  1.1900        unfolding algebraic_closure_axioms_def by auto
  1.1901 @@ -764,5 +2048,161 @@
  1.1902    using exists_closure unfolding closure_def
  1.1903    by (metis (mono_tags, lifting) someI2)+
  1.1904  
  1.1905 +lemma (in field) algebraically_closedI:
  1.1906 +  assumes "\<And>p. \<lbrakk> p \<in> carrier (poly_ring R); degree p > 1 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier R. eval p x = \<zero>"
  1.1907 +  shows "algebraically_closed R"
  1.1908 +proof
  1.1909 +  fix p assume "p \<in> carrier (poly_ring R)" thus "splitted p"
  1.1910 +  proof (induction "degree p" arbitrary: p rule: less_induct)
  1.1911 +    case less show ?case
  1.1912 +    proof (cases "degree p \<le> 1")
  1.1913 +      case True with \<open>p \<in> carrier (poly_ring R)\<close> show ?thesis
  1.1914 +        using degree_zero_imp_splitted degree_one_imp_splitted by fastforce
  1.1915 +    next
  1.1916 +      case False then have "degree p > 1"
  1.1917 +        by simp
  1.1918 +      with \<open>p \<in> carrier (poly_ring R)\<close> have "roots p \<noteq> {#}"
  1.1919 +        using assms[of p] roots_mem_iff_is_root[of p] unfolding is_root_def by force
  1.1920 +      then obtain a where a: "a \<in> carrier R" "a \<in># roots p"
  1.1921 +        and pdiv: "[ \<one>, \<ominus> a ] pdivides p" and in_carrier: "[ \<one>, \<ominus> a ] \<in> carrier (poly_ring R)"
  1.1922 +        using less(2) by blast
  1.1923 +      then obtain q where q: "q \<in> carrier (poly_ring R)" and p: "p = [ \<one>, \<ominus> a ] \<otimes>\<^bsub>poly_ring R\<^esub> q"
  1.1924 +        unfolding pdivides_def by blast
  1.1925 +      with \<open>degree p > 1\<close> have not_zero: "q \<noteq> []" and "p \<noteq> []"
  1.1926 +        using domain.integral_iff[OF univ_poly_is_domain[OF carrier_is_subring] in_carrier, of q]
  1.1927 +        by (auto simp add: univ_poly_zero[of R "carrier R"])
  1.1928 +      hence deg: "degree p = Suc (degree q)"
  1.1929 +        using poly_mult_degree_eq[OF carrier_is_subring] in_carrier q p
  1.1930 +        unfolding univ_poly_carrier sym[OF univ_poly_mult[of R "carrier R"]] by auto
  1.1931 +      hence "splitted q"
  1.1932 +        using less(1)[OF _ q] by simp
  1.1933 +      moreover have "roots p = add_mset a (roots q)"
  1.1934 +        using poly_mult_degree_one_monic_imp_same_roots[OF a(1) q not_zero] p by simp
  1.1935 +      ultimately show ?thesis
  1.1936 +        unfolding splitted_def deg by simp
  1.1937 +    qed
  1.1938 +  qed
  1.1939 +qed
  1.1940 +
  1.1941 +sublocale algebraic_closure \<subseteq> algebraically_closed
  1.1942 +proof (rule algebraically_closedI)
  1.1943 +  fix P assume in_carrier: "P \<in> carrier (poly_ring L)" and gt_one: "degree P > 1"
  1.1944 +  then have gt_zero: "degree P > 0"
  1.1945 +    by simp
  1.1946 +
  1.1947 +  define A where "A = finite_extension K P"
  1.1948 +
  1.1949 +  from \<open>P \<in> carrier (poly_ring L)\<close> have "set P \<subseteq> carrier L"
  1.1950 +    by (simp add: polynomial_incl univ_poly_carrier)
  1.1951 +  hence A: "subfield A L" and P: "P \<in> carrier (A[X])"
  1.1952 +    using finite_extension_mem[OF subfieldE(1)[OF subfield_axioms], of P] in_carrier
  1.1953 +          algebraic_extension finite_extension_is_subfield[OF subfield_axioms, of P]
  1.1954 +    unfolding sym[OF A_def] sym[OF univ_poly_carrier] polynomial_def by auto
  1.1955 +  from \<open>set P \<subseteq> carrier L\<close> have incl: "K \<subseteq> A"
  1.1956 +    using finite_extension_incl[OF subfieldE(3)[OF subfield_axioms]] unfolding A_def by simp
  1.1957 +
  1.1958 +  interpret UP_K: domain "K[X]"
  1.1959 +    using univ_poly_is_domain[OF subfieldE(1)[OF subfield_axioms]] .
  1.1960 +  interpret UP_A: domain "A[X]"
  1.1961 +    using univ_poly_is_domain[OF subfieldE(1)[OF A]] .
  1.1962 +  interpret Rupt: ring "Rupt A P"
  1.1963 +    unfolding rupture_def using ideal.quotient_is_ring[OF UP_A.cgenideal_ideal[OF P]] .
  1.1964 +  interpret Hom: ring_hom_ring "L \<lparr> carrier := A \<rparr>" "Rupt A P" "rupture_surj A P \<circ> poly_of_const"
  1.1965 +    using ring_hom_ringI2[OF subring_is_ring[OF subfieldE(1)] Rupt.ring_axioms
  1.1966 +          rupture_surj_norm_is_hom[OF subfieldE(1) P]] A by simp
  1.1967 +  let ?h = "rupture_surj A P \<circ> poly_of_const"
  1.1968 +
  1.1969 +  have h_simp: "rupture_surj A P ` poly_of_const ` E = ?h ` E" for E
  1.1970 +    by auto
  1.1971 +  hence aux_lemmas:
  1.1972 +    "subfield (rupture_surj A P ` poly_of_const ` K) (Rupt A P)"
  1.1973 +    "subfield (rupture_surj A P ` poly_of_const ` A) (Rupt A P)"
  1.1974 +    using Hom.img_is_subfield(2)[OF _ rupture_one_not_zero[OF A P gt_zero]]
  1.1975 +          ring.subfield_iff(1)[OF subring_is_ring[OF subfieldE(1)[OF A]]]
  1.1976 +          subfield_iff(2)[OF subfield_axioms] subfield_iff(2)[OF A] incl
  1.1977 +    by auto
  1.1978 +
  1.1979 +  have "carrier (K[X]) \<subseteq> carrier (A[X])"
  1.1980 +    using subsetI[of "carrier (K[X])" "carrier (A[X])"] incl
  1.1981 +    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  1.1982 +  hence "id \<in> ring_hom (K[X]) (A[X])"
  1.1983 +    unfolding ring_hom_def unfolding univ_poly_mult univ_poly_add univ_poly_one by (simp add: subsetD)
  1.1984 +  hence "rupture_surj A P \<in> ring_hom (K[X]) (Rupt A P)"
  1.1985 +    using ring_hom_trans[OF _ rupture_surj_hom(1)[OF subfieldE(1)[OF A] P], of id] by simp
  1.1986 +  then interpret Hom': ring_hom_ring "K[X]" "Rupt A P" "rupture_surj A P"
  1.1987 +    using ring_hom_ringI2[OF UP_K.ring_axioms Rupt.ring_axioms] by simp
  1.1988 +
  1.1989 +  from \<open>id \<in> ring_hom (K[X]) (A[X])\<close> have Id: "ring_hom_ring (K[X]) (A[X]) id"
  1.1990 +    using ring_hom_ringI2[OF UP_K.ring_axioms UP_A.ring_axioms] by simp
  1.1991 +  hence "subalgebra (poly_of_const ` K) (carrier (K[X])) (A[X])"
  1.1992 +    using ring_hom_ring.img_is_subalgebra[OF Id _ UP_K.carrier_is_subalgebra[OF subfieldE(3)]]
  1.1993 +          univ_poly_subfield_of_consts[OF subfield_axioms] by auto
  1.1994 +
  1.1995 +  moreover from \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "poly_of_const ` K \<subseteq> carrier (A[X])"
  1.1996 +    using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp
  1.1997 +
  1.1998 +  ultimately
  1.1999 +  have "subalgebra (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X])) (Rupt A P)"
  1.2000 +    using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp
  1.2001 +
  1.2002 +  moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carrier (Rupt A P))"
  1.2003 +  proof (intro Rupt.telescopic_base_dim(1)[where
  1.2004 +            ?K = "rupture_surj A P ` poly_of_const ` K" and
  1.2005 +            ?F = "rupture_surj A P ` poly_of_const ` A" and
  1.2006 +            ?E = "carrier (Rupt A P)", OF aux_lemmas])
  1.2007 +    show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` A) (carrier (Rupt A P))"
  1.2008 +      using Rupt.finite_dimensionI[OF rupture_dimension[OF A P gt_zero]] .
  1.2009 +  next
  1.2010 +    let ?h = "rupture_surj A P \<circ> poly_of_const"
  1.2011 +
  1.2012 +    from \<open>set P \<subseteq> carrier L\<close> have "finite_dimension K A"
  1.2013 +      using finite_extension_finite_dimension(1)[OF subfield_axioms, of P] algebraic_extension
  1.2014 +      unfolding A_def by auto
  1.2015 +    then obtain Us where Us: "set Us \<subseteq> carrier L" "A = Span K Us"
  1.2016 +      using exists_base subfield_axioms by blast
  1.2017 +    hence "?h ` A = Rupt.Span (?h ` K) (map ?h Us)"
  1.2018 +      using Hom.Span_hom[of K Us] incl Span_base_incl[OF subfield_axioms, of Us]
  1.2019 +      unfolding Span_consistent[OF subfieldE(1)[OF A]] by simp
  1.2020 +    moreover have "set (map ?h Us) \<subseteq> carrier (Rupt A P)"
  1.2021 +      using Span_base_incl[OF subfield_axioms Us(1)] ring_hom_memE(1)[OF Hom.homh]
  1.2022 +      unfolding sym[OF Us(2)] by auto
  1.2023 +    ultimately
  1.2024 +    show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` poly_of_const ` A)"
  1.2025 +      using Rupt.Span_finite_dimension[OF aux_lemmas(1)] unfolding h_simp by simp
  1.2026 +  qed
  1.2027 +
  1.2028 +  moreover have "rupture_surj A P ` carrier (A[X]) = carrier (Rupt A P)"
  1.2029 +    unfolding rupture_def FactRing_def A_RCOSETS_def' by auto
  1.2030 +  with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "rupture_surj A P ` carrier (K[X]) \<subseteq> carrier (Rupt A P)"
  1.2031 +    by auto
  1.2032 +
  1.2033 +  ultimately
  1.2034 +  have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X]))"
  1.2035 +    using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp
  1.2036 +
  1.2037 +  hence "\<not> inj_on (rupture_surj A P) (carrier (K[X]))"
  1.2038 +    using Hom'.infinite_dimension_hom[OF _ rupture_one_not_zero[OF A P gt_zero] _
  1.2039 +          UP_K.carrier_is_subalgebra[OF subfieldE(3)] univ_poly_infinite_dimension[OF subfield_axioms]]
  1.2040 +          univ_poly_subfield_of_consts[OF subfield_axioms]
  1.2041 +    by auto
  1.2042 +  then obtain Q where Q: "Q \<in> carrier (K[X])" "Q \<noteq> []" and "rupture_surj A P Q = \<zero>\<^bsub>Rupt A P\<^esub>"
  1.2043 +    using Hom'.trivial_ker_imp_inj Hom'.hom_zero unfolding a_kernel_def' univ_poly_zero by blast
  1.2044 +  with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "Q \<in> PIdl\<^bsub>A[X]\<^esub> P"
  1.2045 +    using ideal.rcos_const_imp_mem[OF UP_A.cgenideal_ideal[OF P]]
  1.2046 +    unfolding rupture_def FactRing_def by auto
  1.2047 +  then obtain R where "R \<in> carrier (A[X])" and "Q = R \<otimes>\<^bsub>A[X]\<^esub> P"
  1.2048 +    unfolding cgenideal_def by blast
  1.2049 +  with \<open>P \<in> carrier (A[X])\<close> have "P pdivides Q"
  1.2050 +    using dividesI[of _ "A[X]"] UP_A.m_comm pdivides_iff_shell[OF A] by simp
  1.2051 +  hence "splitted P"
  1.2052 +    using pdivides_imp_splitted[OF in_carrier
  1.2053 +          carrier_polynomial_shell[OF subfieldE(1)[OF subfield_axioms] Q(1)] Q(2)
  1.2054 +          roots_over_subfield[OF Q(1)]] Q by simp
  1.2055 +  with \<open>degree P > 1\<close> obtain a where "a \<in># roots P"
  1.2056 +    unfolding splitted_def by force
  1.2057 +  thus "\<exists>x\<in>carrier L. eval P x = \<zero>"
  1.2058 +    unfolding roots_mem_iff_is_root[OF in_carrier] is_root_def by blast
  1.2059 +qed
  1.2060 +
  1.2061  end
  1.2062 -  
  1.2063 +