author paulson Mon Apr 29 16:50:20 2019 +0100 (6 months ago) changeset 70212 e886b58bf698 parent 70196 b7ef9090feed child 70213 ff8386fc191d
full proof of algebraic closure, by Paulo de Vilhena
```     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.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.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.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.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 +
```