moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory

--- a/CONTRIBUTORS	Thu Apr 04 11:40:45 2024 +0200
+++ b/CONTRIBUTORS	Thu Apr 04 15:29:41 2024 +0200
@@ -6,6 +6,11 @@
 Contributions to Isabelle2024
 -----------------------------
 
+* Αpril 2024: Manuel Eberl, Katharina Kreuzer
+  Some material on finite fields and the characteristic of a ring in HOL,
+  HOL-Computational_Algebra, and HOL-Number_Theory.
+  Also a type constructor for the algebraic closure of a field.
+
 * March 2024: Manuel Eberl
   Weierstraß Factorization Theorem in HOL-Complex_Analysis.
 

--- a/src/HOL/Algebra/Algebra.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Algebra/Algebra.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -5,4 +5,5 @@
      Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
      Left_Coset SimpleGroups SndIsomorphismGrp
 begin
+
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Algebraic_Closure_Type.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -0,0 +1,625 @@
+(*
+  File:      Algebra/Algebraic_Closure_Type.thy
+  Authors:   Katharina Kreuzer (TU München)
+             Manuel Eberl (University of Innsbruck)
+
+  A type definition for the algebraic closure of fields.
+*)
+
+theory Algebraic_Closure_Type
+imports
+  Algebraic_Closure
+  "HOL-Computational_Algebra.Computational_Algebra"
+  "HOL-Computational_Algebra.Field_as_Ring"
+begin
+
+
+definition (in ring_1) ring_of_type_algebra :: "'a ring"
+  where "ring_of_type_algebra = \<lparr> 
+    carrier = UNIV, monoid.mult = (\<lambda>x y. x * y),  
+    one = 1,
+    ring.zero = 0,
+    add = (\<lambda> x y. x + y) \<rparr>"
+
+lemma (in comm_ring_1) ring_from_type_algebra [intro]:
+  "ring (ring_of_type_algebra :: 'a ring)"
+proof -
+  have "\<exists>y. x + y = 0" for x :: 'a
+    using add.right_inverse by blast
+  thus ?thesis
+    unfolding ring_of_type_algebra_def using add.right_inverse
+    by unfold_locales (auto simp:algebra_simps Units_def)
+qed
+
+lemma (in comm_ring_1) cring_from_type_algebra [intro]:
+  "cring (ring_of_type_algebra :: 'a ring)"
+proof -
+  have "\<exists>y. x + y = 0" for x :: 'a
+    using add.right_inverse by blast
+  thus ?thesis
+    unfolding ring_of_type_algebra_def using add.right_inverse
+    by unfold_locales (auto simp:algebra_simps Units_def)
+qed
+
+lemma (in Fields.field) field_from_type_algebra [intro]:
+  "field (ring_of_type_algebra :: 'a ring)"
+proof -
+  have "\<exists>y. x + y = 0" for x :: 'a
+    using add.right_inverse by blast
+
+  moreover have "x \<noteq> 0 \<Longrightarrow> \<exists>y. x * y = 1" for x :: 'a
+    by (rule exI[of _ "inverse x"]) auto
+
+  ultimately show ?thesis
+    unfolding ring_of_type_algebra_def using add.right_inverse
+    by unfold_locales (auto simp:algebra_simps Units_def)
+qed
+
+
+
+subsection \<open>Definition\<close>
+
+typedef (overloaded) 'a :: field alg_closure =
+  "carrier (field.alg_closure (ring_of_type_algebra :: 'a :: field ring))"
+proof -
+  define K where "K \<equiv> (ring_of_type_algebra :: 'a ring)"
+  define L where "L \<equiv> field.alg_closure K"
+
+  interpret K: field K
+    unfolding K_def by rule
+
+  interpret algebraic_closure L "range K.indexed_const"
+  proof -
+    have *: "carrier K = UNIV"
+      by (auto simp: K_def ring_of_type_algebra_def)
+    show "algebraic_closure L (range K.indexed_const)"
+      unfolding * [symmetric] L_def by (rule K.alg_closureE)
+  qed
+
+  show "\<exists>x. x \<in> carrier L"
+    using zero_closed by blast
+qed
+
+setup_lifting type_definition_alg_closure
+
+instantiation alg_closure :: (field) field
+begin
+
+context
+  fixes L K
+  defines "K \<equiv> (ring_of_type_algebra :: 'a :: field ring)"
+  defines "L \<equiv> field.alg_closure K"
+begin
+
+interpretation K: field K
+  unfolding K_def by rule
+
+interpretation algebraic_closure L "range K.indexed_const"
+proof -
+  have *: "carrier K = UNIV"
+    by (auto simp: K_def ring_of_type_algebra_def)
+  show "algebraic_closure L (range K.indexed_const)"
+    unfolding * [symmetric] L_def by (rule K.alg_closureE)
+qed
+
+lift_definition zero_alg_closure :: "'a alg_closure" is "ring.zero L"
+  by (fold K_def, fold L_def) (rule ring_simprules)
+
+lift_definition one_alg_closure :: "'a alg_closure" is "monoid.one L"
+  by (fold K_def, fold L_def) (rule ring_simprules)
+
+lift_definition plus_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure \<Rightarrow> 'a alg_closure"
+  is "ring.add L"
+  by (fold K_def, fold L_def) (rule ring_simprules)
+
+lift_definition minus_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure \<Rightarrow> 'a alg_closure"
+  is "a_minus L"
+  by (fold K_def, fold L_def) (rule ring_simprules)
+
+lift_definition times_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure \<Rightarrow> 'a alg_closure"
+  is "monoid.mult L"
+  by (fold K_def, fold L_def) (rule ring_simprules)
+
+lift_definition uminus_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure"
+  is "a_inv L"
+  by (fold K_def, fold L_def) (rule ring_simprules)
+
+lift_definition inverse_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure"
+  is "\<lambda>x. if x = ring.zero L then ring.zero L else m_inv L x"
+  by (fold K_def, fold L_def) (auto simp: field_Units)
+
+lift_definition divide_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure \<Rightarrow> 'a alg_closure"
+  is "\<lambda>x y. if y = ring.zero L then ring.zero L else monoid.mult L x (m_inv L y)"
+  by (fold K_def, fold L_def) (auto simp: field_Units)
+
+end
+
+instance proof -
+  define K where "K \<equiv> (ring_of_type_algebra :: 'a ring)"
+  define L where "L \<equiv> field.alg_closure K"
+
+  interpret K: field K
+    unfolding K_def by rule
+
+  interpret algebraic_closure L "range K.indexed_const"
+  proof -
+    have *: "carrier K = UNIV"
+      by (auto simp: K_def ring_of_type_algebra_def)
+    show "algebraic_closure L (range K.indexed_const)"
+      unfolding * [symmetric] L_def by (rule K.alg_closureE)
+  qed
+
+  show "OFCLASS('a alg_closure, field_class)"
+  proof (standard, goal_cases)
+    case 1
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule m_assoc)
+  next
+    case 2
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule m_comm)
+  next
+    case 3
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule l_one)
+  next
+    case 4
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule a_assoc)
+  next
+    case 5
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule a_comm)
+  next
+    case 6
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule l_zero)
+  next
+    case 7
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule ring_simprules)
+  next
+    case 8
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule ring_simprules)
+  next
+    case 9
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule ring_simprules)
+  next
+    case 10
+    show ?case
+      by (transfer, fold K_def, fold L_def) (rule zero_not_one)
+  next
+    case 11
+    thus ?case
+      by (transfer, fold K_def, fold L_def) (auto simp: field_Units)
+  next
+    case 12
+    thus ?case
+      by (transfer, fold K_def, fold L_def) auto
+  next
+    case 13
+    thus ?case
+      by transfer auto
+  qed
+qed
+
+end
+
+
+
+subsection \<open>The algebraic closure is algebraically closed\<close>
+
+instance alg_closure :: (field) alg_closed_field
+proof
+  define K where "K \<equiv> (ring_of_type_algebra :: 'a ring)"
+  define L where "L \<equiv> field.alg_closure K"
+
+  interpret K: field K
+    unfolding K_def by rule
+
+  interpret algebraic_closure L "range K.indexed_const"
+  proof -
+    have *: "carrier K = UNIV"
+      by (auto simp: K_def ring_of_type_algebra_def)
+    show "algebraic_closure L (range K.indexed_const)"
+      unfolding * [symmetric] L_def by (rule K.alg_closureE)
+  qed
+
+  have [simp]: "Rep_alg_closure x \<in> carrier L" for x
+    using Rep_alg_closure[of x] by (simp only: L_def K_def)
+
+  have [simp]: "Rep_alg_closure x = Rep_alg_closure y \<longleftrightarrow> x = y" for x y
+    by (simp add: Rep_alg_closure_inject)
+  have [simp]: "Rep_alg_closure x = \<zero>\<^bsub>L\<^esub> \<longleftrightarrow> x = 0" for x
+  proof -
+    have "Rep_alg_closure x = Rep_alg_closure 0 \<longleftrightarrow> x = 0"
+      by simp
+    also have "Rep_alg_closure 0 = \<zero>\<^bsub>L\<^esub>"
+      by (simp add: zero_alg_closure.rep_eq L_def K_def)
+    finally show ?thesis .
+  qed
+
+  have [simp]: "Rep_alg_closure (x ^ n) = Rep_alg_closure x [^]\<^bsub>L\<^esub> n"
+    for x :: "'a alg_closure" and n
+    by (induction n)
+       (auto simp: one_alg_closure.rep_eq times_alg_closure.rep_eq m_comm
+             simp flip: L_def K_def)
+  have [simp]: "Rep_alg_closure (Abs_alg_closure x) = x" if "x \<in> carrier L" for x
+    using that unfolding L_def K_def by (rule Abs_alg_closure_inverse)
+
+  show "\<exists>x. poly p x = 0" if p: "Polynomial.lead_coeff p = 1" "Polynomial.degree p > 0"
+    for p :: "'a alg_closure poly"
+  proof -
+    define P where "P = rev (map Rep_alg_closure (Polynomial.coeffs p))"
+    have deg: "Polynomials.degree P = Polynomial.degree p"
+      by (auto simp: P_def degree_eq_length_coeffs)
+    have carrier_P: "P \<in> carrier (poly_ring L)"
+      by (auto simp: univ_poly_def polynomial_def P_def hd_map hd_rev last_map 
+                     last_coeffs_eq_coeff_degree)
+    hence "splitted P"
+      using roots_over_carrier by blast
+    hence "roots P \<noteq> {#}"
+      unfolding splitted_def using deg p by auto
+    then obtain x where "x \<in># roots P"
+      by blast
+    hence x: "is_root P x"
+      using roots_mem_iff_is_root[OF carrier_P] by auto
+    hence [simp]: "x \<in> carrier L"
+      by (auto simp: is_root_def)
+    define x' where "x' = Abs_alg_closure x"
+    define xs where "xs = rev (coeffs p)"
+
+    have "cr_alg_closure (eval (map Rep_alg_closure xs) x) (poly (Poly (rev xs)) x')"
+      by (induction xs)
+         (auto simp flip: K_def L_def simp: cr_alg_closure_def
+                 zero_alg_closure.rep_eq plus_alg_closure.rep_eq
+                 times_alg_closure.rep_eq Poly_append poly_monom
+                 a_comm m_comm x'_def)
+    also have "map Rep_alg_closure xs = P"
+      by (simp add: xs_def P_def rev_map)
+    also have "Poly (rev xs) = p"
+      by (simp add: xs_def)
+    finally have "poly p x' = 0"
+      using x by (auto simp: is_root_def cr_alg_closure_def)
+    thus "\<exists>x. poly p x = 0" ..
+  qed
+qed
+
+
+
+subsection \<open>Converting between the base field and the closure\<close>
+
+context
+  fixes L K
+  defines "K \<equiv> (ring_of_type_algebra :: 'a :: field ring)"
+  defines "L \<equiv> field.alg_closure K"
+begin
+
+interpretation K: field K
+  unfolding K_def by rule
+
+interpretation algebraic_closure L "range K.indexed_const"
+proof -
+  have *: "carrier K = UNIV"
+    by (auto simp: K_def ring_of_type_algebra_def)
+  show "algebraic_closure L (range K.indexed_const)"
+    unfolding * [symmetric] L_def by (rule K.alg_closureE)
+qed
+
+lemma alg_closure_hom: "K.indexed_const \<in> Ring.ring_hom K L"
+  unfolding L_def using K.alg_closureE(2) .
+
+lift_definition%important to_ac :: "'a :: field \<Rightarrow> 'a alg_closure"
+  is "ring.indexed_const K"
+  by (fold K_def, fold L_def) (use mem_carrier in blast)
+
+lemma to_ac_0 [simp]: "to_ac (0 :: 'a) = 0"
+proof -
+  have "to_ac (\<zero>\<^bsub>K\<^esub>) = 0"
+  proof (transfer fixing: K, fold K_def, fold L_def)
+    show "K.indexed_const \<zero>\<^bsub>K\<^esub> = \<zero>\<^bsub>L\<^esub>"
+      using Ring.ring_hom_zero[OF alg_closure_hom] K.ring_axioms is_ring
+      by simp
+  qed
+  thus ?thesis
+    by (simp add: K_def ring_of_type_algebra_def)
+qed
+
+lemma to_ac_1 [simp]: "to_ac (1 :: 'a) = 1"
+proof -
+  have "to_ac (\<one>\<^bsub>K\<^esub>) = 1"
+  proof (transfer fixing: K, fold K_def, fold L_def)
+    show "K.indexed_const \<one>\<^bsub>K\<^esub> = \<one>\<^bsub>L\<^esub>"
+      using Ring.ring_hom_one[OF alg_closure_hom] K.ring_axioms is_ring
+      by simp
+  qed
+  thus ?thesis
+    by (simp add: K_def ring_of_type_algebra_def)
+qed
+
+lemma to_ac_add [simp]: "to_ac (x + y :: 'a) = to_ac x + to_ac y"
+proof -
+  have "to_ac (x \<oplus>\<^bsub>K\<^esub> y) = to_ac x + to_ac y"
+  proof (transfer fixing: K x y, fold K_def, fold L_def)
+    show "K.indexed_const (x \<oplus>\<^bsub>K\<^esub> y) = K.indexed_const x \<oplus>\<^bsub>L\<^esub> K.indexed_const y"
+      using Ring.ring_hom_add[OF alg_closure_hom, of x y] K.ring_axioms is_ring
+      by (simp add: K_def ring_of_type_algebra_def)
+  qed
+  thus ?thesis
+    by (simp add: K_def ring_of_type_algebra_def)
+qed
+
+lemma to_ac_minus [simp]: "to_ac (-x :: 'a) = -to_ac x"
+  using to_ac_add to_ac_0 add_eq_0_iff by metis
+
+lemma to_ac_diff [simp]: "to_ac (x - y :: 'a) = to_ac x - to_ac y"
+  using to_ac_add[of x "-y"] by simp
+
+lemma to_ac_mult [simp]: "to_ac (x * y :: 'a) = to_ac x * to_ac y"
+proof -
+  have "to_ac (x \<otimes>\<^bsub>K\<^esub> y) = to_ac x * to_ac y"
+  proof (transfer fixing: K x y, fold K_def, fold L_def)
+    show "K.indexed_const (x \<otimes>\<^bsub>K\<^esub> y) = K.indexed_const x \<otimes>\<^bsub>L\<^esub> K.indexed_const y"
+      using Ring.ring_hom_mult[OF alg_closure_hom, of x y] K.ring_axioms is_ring
+      by (simp add: K_def ring_of_type_algebra_def)
+  qed
+  thus ?thesis
+    by (simp add: K_def ring_of_type_algebra_def)
+qed
+
+lemma to_ac_inverse [simp]: "to_ac (inverse x :: 'a) = inverse (to_ac x)"
+  using to_ac_mult[of x "inverse x"] to_ac_1 to_ac_0
+  by (metis divide_self_if field_class.field_divide_inverse field_class.field_inverse_zero inverse_unique)
+
+lemma to_ac_divide [simp]: "to_ac (x / y :: 'a) = to_ac x / to_ac y"
+  using to_ac_mult[of x "inverse y"] to_ac_inverse[of y]
+  by (simp add: field_class.field_divide_inverse)
+
+lemma to_ac_power [simp]: "to_ac (x ^ n) = to_ac x ^ n"
+  by (induction n) auto
+
+lemma to_ac_of_nat [simp]: "to_ac (of_nat n) = of_nat n"
+  by (induction n) auto
+
+lemma to_ac_of_int [simp]: "to_ac (of_int n) = of_int n"
+  by (induction n) auto
+
+lemma to_ac_numeral [simp]: "to_ac (numeral n) = numeral n"
+  using to_ac_of_nat[of "numeral n"] by (simp del: to_ac_of_nat)
+
+lemma to_ac_sum: "to_ac (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. to_ac (f x))"
+  by (induction A rule: infinite_finite_induct) auto
+
+lemma to_ac_prod: "to_ac (\<Prod>x\<in>A. f x) = (\<Prod>x\<in>A. to_ac (f x))"
+  by (induction A rule: infinite_finite_induct) auto
+
+lemma to_ac_sum_list: "to_ac (sum_list xs) = (\<Sum>x\<leftarrow>xs. to_ac x)"
+  by (induction xs) auto
+
+lemma to_ac_prod_list: "to_ac (prod_list xs) = (\<Prod>x\<leftarrow>xs. to_ac x)"
+  by (induction xs) auto
+
+lemma to_ac_sum_mset: "to_ac (sum_mset xs) = (\<Sum>x\<in>#xs. to_ac x)"
+  by (induction xs) auto
+
+lemma to_ac_prod_mset: "to_ac (prod_mset xs) = (\<Prod>x\<in>#xs. to_ac x)"
+  by (induction xs) auto
+
+end
+
+lemma (in ring) indexed_const_eq_iff [simp]:
+  "indexed_const x = (indexed_const y :: 'c multiset \<Rightarrow> 'a) \<longleftrightarrow> x = y"
+proof
+  assume "indexed_const x = (indexed_const y :: 'c multiset \<Rightarrow> 'a)"
+  hence "indexed_const x ({#} :: 'c multiset) = indexed_const y ({#} :: 'c multiset)"
+    by metis
+  thus "x = y"
+    by (simp add: indexed_const_def)
+qed auto
+
+lemma inj_to_ac: "inj to_ac"
+  by (transfer, intro injI, subst (asm) ring.indexed_const_eq_iff) auto
+
+lemma to_ac_eq_iff [simp]: "to_ac x = to_ac y \<longleftrightarrow> x = y"
+  using inj_to_ac by (auto simp: inj_on_def)
+
+lemma to_ac_eq_0_iff [simp]: "to_ac x = 0 \<longleftrightarrow> x = 0"
+  and to_ac_eq_0_iff' [simp]: "0 = to_ac x \<longleftrightarrow> x = 0"
+  and to_ac_eq_1_iff [simp]: "to_ac x = 1 \<longleftrightarrow> x = 1"
+  and to_ac_eq_1_iff' [simp]: "1 = to_ac x \<longleftrightarrow> x = 1"
+  using to_ac_eq_iff to_ac_0 to_ac_1 by metis+
+
+
+definition of_ac :: "'a :: field alg_closure \<Rightarrow> 'a" where
+  "of_ac x = (if x \<in> range to_ac then inv_into UNIV to_ac x else 0)"
+
+lemma of_ac_eqI: "to_ac x = y \<Longrightarrow> of_ac y = x"
+  unfolding of_ac_def by (meson inj_to_ac inv_f_f range_eqI)
+
+lemma of_ac_0 [simp]: "of_ac 0 = 0"
+  and of_ac_1 [simp]: "of_ac 1 = 1"
+  by (rule of_ac_eqI; simp; fail)+
+
+lemma of_ac_to_ac [simp]: "of_ac (to_ac x) = x"
+  by (rule of_ac_eqI) auto
+
+lemma to_ac_of_ac: "x \<in> range to_ac \<Longrightarrow> to_ac (of_ac x) = x"
+  by auto
+
+
+lemma CHAR_alg_closure [simp]:
+  "CHAR('a :: field alg_closure) = CHAR('a)"
+proof (rule CHAR_eqI)
+  show "of_nat CHAR('a) = (0 :: 'a alg_closure)"
+    by (metis of_nat_CHAR to_ac_0 to_ac_of_nat)
+next
+  show "CHAR('a) dvd n" if "of_nat n = (0 :: 'a alg_closure)" for n
+    using that by (metis of_nat_eq_0_iff_char_dvd to_ac_eq_0_iff' to_ac_of_nat)
+qed
+
+instance alg_closure :: (field_char_0) field_char_0
+proof
+  show "inj (of_nat :: nat \<Rightarrow> 'a alg_closure)"
+    by (metis injD inj_of_nat inj_on_def inj_to_ac to_ac_of_nat)
+qed
+
+
+bundle alg_closure_syntax
+begin
+notation to_ac ("_\<up>" [1000] 999)
+notation of_ac ("_\<down>" [1000] 999)
+end
+
+
+bundle alg_closure_syntax'
+begin
+notation (output) to_ac ("_")
+notation (output) of_ac ("_")
+end
+
+
+subsection \<open>The algebraic closure is an algebraic extension\<close>
+
+text \<open>
+  The algebraic closure is an algebraic extension, i.e.\ every element in it is
+  a root of some non-zero polynomial in the base field.
+\<close>
+theorem alg_closure_algebraic:
+  fixes x :: "'a :: field alg_closure"
+  obtains p :: "'a poly" where "p \<noteq> 0" "poly (map_poly to_ac p) x = 0"
+proof -
+  define K where "K \<equiv> (ring_of_type_algebra :: 'a ring)"
+  define L where "L \<equiv> field.alg_closure K"
+
+  interpret K: field K
+    unfolding K_def by rule
+
+  interpret algebraic_closure L "range K.indexed_const"
+  proof -
+    have *: "carrier K = UNIV"
+      by (auto simp: K_def ring_of_type_algebra_def)
+    show "algebraic_closure L (range K.indexed_const)"
+      unfolding * [symmetric] L_def by (rule K.alg_closureE)
+  qed
+
+  let ?K = "range K.indexed_const"
+  have sr: "subring ?K L"
+    by (rule subring_axioms)
+  define x' where "x' = Rep_alg_closure x"
+  have "x' \<in> carrier L"
+    unfolding x'_def L_def K_def by (rule Rep_alg_closure)
+  hence alg: "(algebraic over range K.indexed_const) x'"
+    using algebraic_extension by blast
+  then obtain p where p: "p \<in> carrier (?K[X]\<^bsub>L\<^esub>)" "p \<noteq> []" "eval p x' = \<zero>\<^bsub>L\<^esub>"
+    using algebraicE[OF sr \<open>x' \<in> carrier L\<close> alg] by blast
+
+  have [simp]: "Rep_alg_closure x \<in> carrier L" for x
+    using Rep_alg_closure[of x] by (simp only: L_def K_def)
+  have [simp]: "Abs_alg_closure x = 0 \<longleftrightarrow> x = \<zero>\<^bsub>L\<^esub>" if "x \<in> carrier L" for x
+    using that unfolding L_def K_def
+    by (metis Abs_alg_closure_inverse zero_alg_closure.rep_eq zero_alg_closure_def)
+  have [simp]: "Rep_alg_closure (x ^ n) = Rep_alg_closure x [^]\<^bsub>L\<^esub> n"
+    for x :: "'a alg_closure" and n
+    by (induction n)
+       (auto simp: one_alg_closure.rep_eq times_alg_closure.rep_eq m_comm
+             simp flip: L_def K_def)
+  have [simp]: "Rep_alg_closure (Abs_alg_closure x) = x" if "x \<in> carrier L" for x
+    using that unfolding L_def K_def by (rule Abs_alg_closure_inverse)
+  have [simp]: "Rep_alg_closure x = \<zero>\<^bsub>L\<^esub> \<longleftrightarrow> x = 0" for x
+    by (metis K_def L_def Rep_alg_closure_inverse zero_alg_closure.rep_eq)
+
+  define p' where "p' = Poly (map Abs_alg_closure (rev p))"
+  have "p' \<noteq> 0"
+  proof
+    assume "p' = 0"
+    then obtain n where n: "map Abs_alg_closure (rev p) = replicate n 0"
+      by (auto simp: p'_def Poly_eq_0)
+    with \<open>p \<noteq> []\<close> have "n > 0"
+      by (auto intro!: Nat.gr0I)
+    have "last (map Abs_alg_closure (rev p)) = 0"
+      using \<open>n > 0\<close> by (subst n) auto
+    moreover have "Polynomials.lead_coeff p \<noteq> \<zero>\<^bsub>L\<^esub>" "Polynomials.lead_coeff p \<in> carrier L"
+      using p \<open>p \<noteq> []\<close> local.subset
+      by (fastforce simp: polynomial_def univ_poly_def)+
+    ultimately show False
+      using \<open>p \<noteq> []\<close> by (auto simp: last_map last_rev)
+  qed
+
+  have "set p \<subseteq> carrier L"
+    using local.subset p by (auto simp: univ_poly_def polynomial_def)
+  hence "cr_alg_closure (eval p x') (poly p' x)"
+    unfolding p'_def
+    by (induction p)
+       (auto simp flip: K_def L_def simp: cr_alg_closure_def
+               zero_alg_closure.rep_eq plus_alg_closure.rep_eq
+               times_alg_closure.rep_eq Poly_append poly_monom
+               a_comm m_comm x'_def)
+  hence "poly p' x = 0"
+    using p by (auto simp: cr_alg_closure_def x'_def)
+
+  have coeff_p': "Polynomial.coeff p' i \<in> range to_ac" for i
+  proof (cases "i \<ge> length p")
+    case False
+    have "Polynomial.coeff p' i = Abs_alg_closure (rev p ! i)"
+      unfolding p'_def using False
+      by (auto simp: nth_default_def)
+    moreover have "rev p ! i \<in> ?K"
+      using p(1) False by (auto simp: univ_poly_def polynomial_def rev_nth)
+    ultimately show ?thesis
+      unfolding to_ac.abs_eq K_def by fastforce
+  qed (auto simp: p'_def nth_default_def)
+  
+
+  define p'' where "p'' = map_poly of_ac p'"
+  have p'_eq: "p' = map_poly to_ac p''"
+    by (rule poly_eqI) (auto simp: coeff_map_poly p''_def to_ac_of_ac[OF coeff_p'])
+
+  show ?thesis
+  proof (rule that)
+    show "p'' \<noteq> 0"
+      using \<open>p' \<noteq> 0\<close> by (auto simp: p'_eq)
+  next
+    show "poly (map_poly to_ac p'') x = 0"
+      using \<open>poly p' x = 0\<close> by (simp add: p'_eq)
+  qed
+qed
+
+
+instantiation alg_closure :: (field)
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
+begin
+
+definition [simp]: "normalize_alg_closure = (normalize_field :: 'a alg_closure \<Rightarrow> _)"
+definition [simp]: "unit_factor_alg_closure = (unit_factor_field :: 'a alg_closure \<Rightarrow> _)"
+definition [simp]: "modulo_alg_closure = (mod_field :: 'a alg_closure \<Rightarrow> _)"
+definition [simp]: "euclidean_size_alg_closure = (euclidean_size_field :: 'a alg_closure \<Rightarrow> _)"
+definition [simp]: "division_segment (x :: 'a alg_closure) = 1"
+
+instance
+  by standard
+    (simp_all add: dvd_field_iff field_split_simps split: if_splits)
+
+end
+
+instantiation alg_closure :: (field) euclidean_ring_gcd
+begin
+
+definition gcd_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure \<Rightarrow> 'a alg_closure" where
+  "gcd_alg_closure = Euclidean_Algorithm.gcd"
+definition lcm_alg_closure :: "'a alg_closure \<Rightarrow> 'a alg_closure \<Rightarrow> 'a alg_closure" where
+  "lcm_alg_closure = Euclidean_Algorithm.lcm"
+definition Gcd_alg_closure :: "'a alg_closure set \<Rightarrow> 'a alg_closure" where
+ "Gcd_alg_closure = Euclidean_Algorithm.Gcd"
+definition Lcm_alg_closure :: "'a alg_closure set \<Rightarrow> 'a alg_closure" where
+ "Lcm_alg_closure = Euclidean_Algorithm.Lcm"
+
+instance by standard (simp_all add: gcd_alg_closure_def lcm_alg_closure_def Gcd_alg_closure_def Lcm_alg_closure_def)
+
+end
+
+instance alg_closure :: (field) semiring_gcd_mult_normalize
+  ..
+
+end
\ No newline at end of file

--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -675,4 +675,31 @@
 
 instance int :: normalization_euclidean_semiring_multiplicative ..
 
+lemma (in idom) prime_CHAR_semidom:
+  assumes "CHAR('a) > 0"
+  shows   "prime CHAR('a)"
+proof -
+  have False if ab: "a \<noteq> 1" "b \<noteq> 1" "CHAR('a) = a * b" for a b
+  proof -
+    from assms ab have "a > 0" "b > 0"
+      by (auto intro!: Nat.gr0I)    
+    have "of_nat (a * b) = (0 :: 'a)"
+      using ab by (metis of_nat_CHAR)
+    also have "of_nat (a * b) = (of_nat a :: 'a) * of_nat b"
+      by simp
+    finally have "of_nat a * of_nat b = (0 :: 'a)" .
+    moreover have "of_nat a * of_nat b \<noteq> (0 :: 'a)"
+      using ab \<open>a > 0\<close> \<open>b > 0\<close>
+      by (intro no_zero_divisors) (auto simp: of_nat_eq_0_iff_char_dvd)
+    ultimately show False
+      by contradiction
+  qed
+  moreover have "CHAR('a) > 1"
+    using assms CHAR_not_1' by linarith
+  ultimately have "prime_elem CHAR('a)"
+    by (intro irreducible_imp_prime_elem) (auto simp: Factorial_Ring.irreducible_def)
+  thus ?thesis
+    by (auto simp: prime_def)
+qed
+
 end

--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -51,6 +51,59 @@
     by auto
 qed (use assms in \<open>auto simp: irreducible_def\<close>)
 
+lemma irreducible_multD:
+  assumes l: "irreducible (a*b)"
+  shows "a dvd 1 \<and> irreducible b \<or> b dvd 1 \<and> irreducible a"
+proof-
+  have *: "irreducible b" if l: "irreducible (a*b)" and a: "a dvd 1" for a b :: 'a
+  proof (rule irreducibleI)
+    show "\<not>(b dvd 1)"
+    proof
+      assume "b dvd 1"
+      hence "a * b dvd 1 * 1"
+        using \<open>a dvd 1\<close> by (intro mult_dvd_mono) auto
+      with l show False
+        by (auto simp: irreducible_def)
+    qed
+  next
+    fix x y assume "b = x * y"
+    have "a * x dvd 1 \<or> y dvd 1"
+      using l by (rule irreducibleD) (use \<open>b = x * y\<close> in \<open>auto simp: mult_ac\<close>)
+    thus "x dvd 1 \<or> y dvd 1"
+      by auto
+  qed (use l a in auto)
+
+  from irreducibleD[OF assms refl] have "a dvd 1 \<or> b dvd 1"
+    by (auto simp: irreducible_def)
+  with *[of a b] *[of b a] l show ?thesis
+    by (auto simp: mult.commute)
+qed
+
+lemma irreducible_power_iff [simp]:
+  "irreducible (p ^ n) \<longleftrightarrow> irreducible p \<and> n = 1"
+proof
+  assume *: "irreducible (p ^ n)"
+  have "irreducible p"
+    using * by (induction n) (auto dest!: irreducible_multD)
+  hence [simp]: "\<not>p dvd 1"
+    using * by (auto simp: irreducible_def)
+
+  consider "n = 0" | "n = 1" | "n > 1"
+    by linarith
+  thus "irreducible p \<and> n = 1"
+  proof cases
+    assume "n > 1"
+    hence "p ^ n = p * p ^ (n - 1)"
+      by (cases n) auto
+    with * \<open>\<not> p dvd 1\<close> have "p ^ (n - 1) dvd 1"
+      using irreducible_multD[of p "p ^ (n - 1)"] by auto
+    with \<open>\<not>p dvd 1\<close> and \<open>n > 1\<close> have False
+      by (meson dvd_power dvd_trans zero_less_diff)
+    thus ?thesis ..
+  qed (use * in auto)
+qed auto
+
+
 definition prime_elem :: "'a \<Rightarrow> bool" where
   "prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
 
@@ -2172,7 +2225,7 @@
   with assms show False by auto
 qed
 
-text \<open>Now a string of results due to Jakub Kądziołka\<close>
+text \<open>Now a string of results due to Maya Kądziołka\<close>
 
 lemma multiplicity_dvd_iff_dvd:
  assumes "x \<noteq> 0"

--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -30,7 +30,7 @@
 
 lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI]
 
-lemma expand_fls_eq: "f = g \<longleftrightarrow> (\<forall>n. f $$ n = g $$ n)"
+lemma fls_eq_iff: "f = g \<longleftrightarrow> (\<forall>n. f $$ n = g $$ n)"
   by (simp add: fls_nth_inject[symmetric] fun_eq_iff)
 
 lemma nth_Abs_fls [simp]: "\<forall>\<^sub>\<infinity>n. f (- int n) = 0 \<Longrightarrow> Abs_fls f $$ n = f n"
@@ -136,9 +136,15 @@
 lemma fls_const_nonzero: "c \<noteq> 0 \<Longrightarrow> fls_const c \<noteq> 0"
   using fls_nonzeroI[of "fls_const c" 0] by simp
 
+lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 \<longleftrightarrow> c = 0"
+  by (auto simp: fls_eq_iff)
+
 lemma fls_const_1 [simp]: "fls_const 1 = 1"
   unfolding fls_const_def one_fls_def ..
 
+lemma fls_const_eq_1_iff [simp]: "fls_const c = 1 \<longleftrightarrow> c = 1"
+  by (auto simp: fls_eq_iff)
+
 lift_definition fls_X :: "'a::{zero,one} fls"
   is "\<lambda>n. if n = 1 then 1 else 0"
   by simp
@@ -1683,6 +1689,18 @@
 
 instance fls :: (idom) idom ..
 
+lemma semiring_char_fls [simp]: "CHAR('a :: comm_semiring_1 fls) = CHAR('a)"
+  by (rule CHAR_eqI) (auto simp: fls_of_nat of_nat_eq_0_iff_char_dvd fls_const_nonzero)
+
+instance fls :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char
+  by (rule semiring_prime_charI) auto
+instance fls :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char
+  by standard
+instance fls :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char
+  by standard
+instance fls :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char
+  by standard
+
 
 subsubsection \<open>Powers\<close>
 
@@ -2908,6 +2926,9 @@
 instance fls :: (field) field
   by (standard, simp_all add: field_simps)
 
+instance fls :: ("{field_prime_char,comm_semiring_1}") field_prime_char
+  by (rule field_prime_charI') auto
+
 
 subsubsection \<open>Division\<close>
 

--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -10,6 +10,7 @@
 imports
   Complex_Main
   Euclidean_Algorithm
+  Primes
 begin
 
 
@@ -537,7 +538,6 @@
 
 instance fps :: (semiring_1_cancel) semiring_1_cancel ..
 
-
 lemma fps_square_nth: "(f^2) $ n = (\<Sum>k\<le>n. f $ k * f $ (n - k))"
   by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost)
 
@@ -562,9 +562,15 @@
 lemma fps_const_nonzero_eq_nonzero: "c \<noteq> 0 \<Longrightarrow> fps_const c \<noteq> 0"
   using fps_nonzeroI[of "fps_const c" 0] by simp
 
+lemma fps_const_eq_0_iff [simp]: "fps_const c = 0 \<longleftrightarrow> c = 0"
+  by (auto simp: fps_eq_iff)
+
 lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1"
   by (simp add: fps_ext)
 
+lemma fps_const_eq_1_iff [simp]: "fps_const c = 1 \<longleftrightarrow> c = 1"
+  by (auto simp: fps_eq_iff)
+
 lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0"
   by (cases "c = 0") (auto intro!: subdegreeI)
 
@@ -681,6 +687,25 @@
 
 instance fps :: (idom) idom ..
 
+lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
+  by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
+
+lemma fps_of_int: "fps_const (of_int c) = of_int c"
+  by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
+                             del: fps_const_minus fps_const_neg)
+
+lemma semiring_char_fps [simp]: "CHAR('a :: comm_semiring_1 fps) = CHAR('a)"
+  by (rule CHAR_eqI) (auto simp flip: fps_of_nat simp: of_nat_eq_0_iff_char_dvd)
+
+instance fps :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char
+  by (rule semiring_prime_charI) auto
+instance fps :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char
+  by standard
+instance fps :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char
+  by standard
+instance fps :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char
+  by standard
+
 lemma fps_numeral_fps_const: "numeral k = fps_const (numeral k)"
   by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1 fps_const_add [symmetric])
 
@@ -699,13 +724,6 @@
 lemma subdegree_numeral [simp]: "subdegree (numeral n) = 0"
   by (simp add: numeral_fps_const)
 
-lemma fps_of_nat: "fps_const (of_nat c) = of_nat c"
-  by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add)
-
-lemma fps_of_int: "fps_const (of_int c) = of_int c"
-  by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] 
-                             del: fps_const_minus fps_const_neg)
-
 lemma fps_nth_of_nat [simp]:
   "(of_nat c) $ n = (if n=0 then of_nat c else 0)"
   by (simp add: fps_of_nat[symmetric])

--- a/src/HOL/Computational_Algebra/Polynomial.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -12,7 +12,7 @@
   Complex_Main
   "HOL-Library.More_List"
   "HOL-Library.Infinite_Set"
-  Factorial_Ring
+  Primes
 begin
 
 context semidom_modulo
@@ -1533,6 +1533,18 @@
 instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0
   by standard (auto simp add: of_nat_poly intro: injI)
 
+lemma semiring_char_poly [simp]: "CHAR('a :: comm_semiring_1 poly) = CHAR('a)"
+  by (rule CHAR_eqI) (auto simp: of_nat_poly of_nat_eq_0_iff_char_dvd)
+
+instance poly :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char
+  by (rule semiring_prime_charI) auto
+instance poly :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char
+  by standard
+instance poly :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char
+  by standard
+instance poly :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char
+  by standard
+
 lemma degree_mult_eq: "p \<noteq> 0 \<Longrightarrow> q \<noteq> 0 \<Longrightarrow> degree (p * q) = degree p + degree q"
   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)
@@ -5940,6 +5952,18 @@
   finally show "\<exists>x. (\<Sum>k\<le>n. f k * x ^ k) = 0" ..
 qed
 
+lemma (in alg_closed_field) nth_root_exists:
+  assumes "n > 0"
+  shows   "\<exists>y. y ^ n = (x :: 'a)"
+proof -
+  define f where "f = (\<lambda>i. if i = 0 then -x else if i = n then 1 else 0)"
+  have "\<exists>x. (\<Sum>k\<le>n. f k * x ^ k) = 0"
+    by (rule alg_closed) (use assms in \<open>auto simp: f_def\<close>)
+  also have "(\<lambda>x. \<Sum>k\<le>n. f k * x ^ k) = (\<lambda>x. \<Sum>k\<in>{0,n}. f k * x ^ k)"
+    by (intro ext sum.mono_neutral_right) (auto simp: f_def)
+  finally show "\<exists>y. y ^ n = x"
+    using assms by (simp add: f_def)
+qed
 
 text \<open>
   We can now prove by induction that every polynomial of degree \<open>n\<close> splits into a product of

--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -632,6 +632,8 @@
                     semiring_gcd_mult_normalize}") euclidean_ring_gcd
   by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard
 
+instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd,
+                    semiring_gcd_mult_normalize}") factorial_semiring_multiplicative ..
   
 subsection \<open>Polynomial GCD\<close>
 

--- a/src/HOL/Computational_Algebra/Primes.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Primes.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -797,6 +797,231 @@
     by (auto simp add: prime_dvd_mult_iff)
 qed
 
+lemma (in ring_1) minus_power_prime_CHAR:
+  assumes "p = CHAR('a)" "prime p"
+  shows "(-x :: 'a) ^ p = -(x ^ p)"
+proof (cases "p = 2")
+  case False
+  have "prime p"
+    using assms by blast
+  hence "odd p"
+    using prime_imp_coprime assms False coprime_right_2_iff_odd gcd_nat.strict_iff_not by blast
+  thus ?thesis
+    by simp
+qed (use assms in \<open>auto simp: uminus_CHAR_2\<close>)
+
+
+subsection \<open>Rings and fields with prime characteristic\<close>
+
+text \<open>
+  We introduce some type classes for rings and fields with prime characteristic.
+\<close>
+
+class semiring_prime_char = semiring_1 +
+  assumes prime_char_aux: "\<exists>n. prime n \<and> of_nat n = (0 :: 'a)"
+begin
+
+lemma CHAR_pos [intro, simp]: "CHAR('a) > 0"
+  using local.CHAR_pos_iff local.prime_char_aux prime_gt_0_nat by blast
+
+lemma CHAR_nonzero [simp]: "CHAR('a) \<noteq> 0"
+  using CHAR_pos by auto
+
+lemma CHAR_prime [intro, simp]: "prime CHAR('a)"
+  by (metis (mono_tags, lifting) gcd_nat.order_iff_strict local.of_nat_1 local.of_nat_eq_0_iff_char_dvd
+        local.one_neq_zero local.prime_char_aux prime_nat_iff)
+
+end
+
+lemma semiring_prime_charI [intro?]:
+  "prime CHAR('a :: semiring_1) \<Longrightarrow> OFCLASS('a, semiring_prime_char_class)"
+  by standard auto
+
+lemma idom_prime_charI [intro?]:
+  assumes "CHAR('a :: idom) > 0"
+  shows   "OFCLASS('a, semiring_prime_char_class)"
+proof
+  show "prime CHAR('a)"
+    using assms prime_CHAR_semidom by blast
+qed
+
+class comm_semiring_prime_char = comm_semiring_1 + semiring_prime_char
+class comm_ring_prime_char = comm_ring_1 + semiring_prime_char
+begin
+subclass comm_semiring_prime_char ..
+end
+class idom_prime_char = idom + semiring_prime_char
+begin
+subclass comm_ring_prime_char ..
+end
+
+class field_prime_char = field +
+  assumes pos_char_exists: "\<exists>n>0. of_nat n = (0 :: 'a)"
+begin
+subclass idom_prime_char
+  apply standard
+  using pos_char_exists local.CHAR_pos_iff local.of_nat_CHAR local.prime_CHAR_semidom by blast
+end
+
+lemma field_prime_charI [intro?]:
+  "n > 0 \<Longrightarrow> of_nat n = (0 :: 'a :: field) \<Longrightarrow> OFCLASS('a, field_prime_char_class)"
+  by standard auto
+
+lemma field_prime_charI' [intro?]:
+  "CHAR('a :: field) > 0 \<Longrightarrow> OFCLASS('a, field_prime_char_class)"
+  by standard auto
+
+
+subsection \<open>Finite fields\<close>
+
+class finite_field = field_prime_char + finite
+
+lemma finite_fieldI [intro?]:
+  assumes "finite (UNIV :: 'a :: field set)"
+  shows   "OFCLASS('a, finite_field_class)"
+proof standard
+  show "\<exists>n>0. of_nat n = (0 :: 'a)"
+    using assms prime_CHAR_semidom[where ?'a = 'a] finite_imp_CHAR_pos[OF assms]
+    by (intro exI[of _ "CHAR('a)"]) auto
+qed fact+
+
+text \<open>
+  On a finite field with \<open>n\<close> elements, taking the \<open>n\<close>-th power of an element
+  is the identity. This is an obvious consequence of the fact that the multiplicative group of
+  the field is a finite group of order \<open>n - 1\<close>, so \<open>x^n = 1\<close> for any non-zero \<open>x\<close>.
+
+  Note that this result is sharp in the sense that the multiplicative group of a
+  finite field is cyclic, i.e.\ it contains an element of order \<open>n - 1\<close>.
+  (We don't prove this here.)
+\<close>
+lemma finite_field_power_card_eq_same:
+  fixes x :: "'a :: finite_field"
+  shows   "x ^ card (UNIV :: 'a set) = x"
+proof (cases "x = 0")
+  case False
+  have "x * (\<Prod>y\<in>UNIV-{0}. x * y) = x * x ^ (card (UNIV :: 'a set) - 1) * \<Prod>(UNIV-{0})"
+    by (simp add: prod.distrib mult_ac)
+  also have "x * x ^ (card (UNIV :: 'a set) - 1) = x ^ Suc (card (UNIV :: 'a set) - 1)"
+    by (subst power_Suc) auto
+  also have "Suc (card (UNIV :: 'a set) - 1) = card (UNIV :: 'a set)"
+    using finite_UNIV_card_ge_0[where ?'a = 'a] by simp
+  also have "(\<Prod>y\<in>UNIV-{0}. x * y) = (\<Prod>y\<in>UNIV-{0}. y)"
+    by (rule prod.reindex_bij_witness[of _ "\<lambda>y. y / x" "\<lambda>y. x * y"]) (use False in auto)
+  finally show ?thesis
+    by simp
+qed (use finite_UNIV_card_ge_0[where ?'a = 'a] in auto)
+
+lemma finite_field_power_card_power_eq_same:
+  fixes x :: "'a :: finite_field"
+  assumes "m = card (UNIV :: 'a set) ^ n"
+  shows   "x ^ m = x"
+  unfolding assms
+  by (induction n) (simp_all add: finite_field_power_card_eq_same power_mult)
+
+class enum_finite_field = finite_field +
+  fixes enum_finite_field :: "nat \<Rightarrow> 'a"
+  assumes enum_finite_field: "enum_finite_field ` {..<card (UNIV :: 'a set)} = UNIV"
+begin
+
+lemma inj_on_enum_finite_field: "inj_on enum_finite_field {..<card (UNIV :: 'a set)}"
+  using enum_finite_field by (simp add: eq_card_imp_inj_on)
+
+end
+
+text \<open>
+  To get rid of the pending sort hypotheses, we prove that the field with 2 elements is indeed
+  a finite field.
+\<close>
+typedef gf2 = "{0, 1 :: nat}"
+  by auto
+
+setup_lifting type_definition_gf2
+
+instantiation gf2 :: field
+begin
+lift_definition zero_gf2 :: "gf2" is "0" by auto
+lift_definition one_gf2 :: "gf2" is "1" by auto
+lift_definition uminus_gf2 :: "gf2 \<Rightarrow> gf2" is "\<lambda>x. x" .
+lift_definition plus_gf2 :: "gf2 \<Rightarrow> gf2 \<Rightarrow> gf2" is "\<lambda>x y. if x = y then 0 else 1" by auto
+lift_definition minus_gf2 :: "gf2 \<Rightarrow> gf2 \<Rightarrow> gf2" is "\<lambda>x y. if x = y then 0 else 1" by auto
+lift_definition times_gf2 :: "gf2 \<Rightarrow> gf2 \<Rightarrow> gf2" is "\<lambda>x y. x * y" by auto
+lift_definition inverse_gf2 :: "gf2 \<Rightarrow> gf2" is "\<lambda>x. x" .
+lift_definition divide_gf2 :: "gf2 \<Rightarrow> gf2 \<Rightarrow> gf2" is "\<lambda>x y. x * y" by auto
+
+instance
+  by standard (transfer; fastforce)+
+
+end
+
+instance gf2 :: finite_field
+proof
+  interpret type_definition Rep_gf2 Abs_gf2 "{0, 1 :: nat}"
+    by (rule type_definition_gf2)
+  show "finite (UNIV :: gf2 set)"
+    by (metis Abs_image finite.emptyI finite.insertI finite_imageI)
+qed
+
+
+subsection \<open>The Freshman's Dream in rings of prime characteristic\<close>
+
+lemma (in comm_semiring_1) freshmans_dream:
+  fixes x y :: 'a and n :: nat
+  assumes "prime CHAR('a)"
+  assumes n_def: "n = CHAR('a)"
+  shows   "(x + y) ^ n = x ^ n + y ^ n"
+proof -
+  interpret comm_semiring_prime_char
+    by standard (auto intro!: exI[of _ "CHAR('a)"] assms)
+  have "n > 0"
+    unfolding n_def by simp
+  have "(x + y) ^ n = (\<Sum>k\<le>n. of_nat (n choose k) * x ^ k * y ^ (n - k))"
+    by (rule binomial_ring)
+  also have "\<dots> = (\<Sum>k\<in>{0,n}. of_nat (n choose k) * x ^ k * y ^ (n - k))"
+  proof (intro sum.mono_neutral_right ballI)
+    fix k assume "k \<in> {..n} - {0, n}"
+    hence k: "k > 0" "k < n"
+      by auto
+    have "CHAR('a) dvd (n choose k)"
+      unfolding n_def
+      by (rule dvd_choose_prime) (use k in \<open>auto simp: n_def\<close>)
+    hence "of_nat (n choose k) = (0 :: 'a)"
+      using of_nat_eq_0_iff_char_dvd by blast
+    thus "of_nat (n choose k) * x ^ k * y ^ (n - k) = 0"
+      by simp
+  qed auto
+  finally show ?thesis
+    using \<open>n > 0\<close> by (simp add: add_ac)
+qed
+
+lemma (in comm_semiring_1) freshmans_dream':
+  assumes [simp]: "prime CHAR('a)" and "m = CHAR('a) ^ n"
+  shows "(x + y :: 'a) ^ m = x ^ m + y ^ m"
+  unfolding assms(2)
+proof (induction n)
+  case (Suc n)
+  have "(x + y) ^ (CHAR('a) ^ n * CHAR('a)) = ((x + y) ^ (CHAR('a) ^ n)) ^ CHAR('a)"
+    by (rule power_mult)
+  thus ?case
+    by (simp add: Suc.IH freshmans_dream Groups.mult_ac flip: power_mult)
+qed auto
+
+lemma (in comm_semiring_1) freshmans_dream_sum:
+  fixes f :: "'b \<Rightarrow> 'a"
+  assumes "prime CHAR('a)" and "n = CHAR('a)"
+  shows "sum f A ^ n = sum (\<lambda>i. f i ^ n) A"
+  using assms
+  by (induct A rule: infinite_finite_induct)
+     (auto simp add: power_0_left freshmans_dream)
+
+lemma (in comm_semiring_1) freshmans_dream_sum':
+  fixes f :: "'b \<Rightarrow> 'a"
+  assumes "prime CHAR('a)" "m = CHAR('a) ^ n"
+  shows   "sum f A ^ m = sum (\<lambda>i. f i ^ m) A"
+  using assms
+  by (induction A rule: infinite_finite_induct)
+     (auto simp: freshmans_dream' power_0_left)
+
+
 
 (* TODO Legacy names *)
 lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]

--- a/src/HOL/GCD.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/GCD.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -2949,4 +2949,98 @@
 lemma (in idom) CHAR_not_1' [simp]: "CHAR('a) \<noteq> Suc 0"
   using local.of_nat_CHAR by fastforce
 
+lemma (in ring_1) uminus_CHAR_2:
+  assumes "CHAR('a) = 2"
+  shows   "-(x :: 'a) = x"
+proof -
+  have "x + x = 2 * x"
+    by (simp add: mult_2)
+  also have "2 = (0 :: 'a)"
+    using assms local.of_nat_CHAR by auto
+  finally show ?thesis
+    by (simp add: add_eq_0_iff2)
+qed
+
+lemma (in ring_1) minus_CHAR_2:
+  assumes "CHAR('a) = 2"
+  shows   "(x - y :: 'a) = x + y"
+proof -
+  have "x - y = x + (-y)"
+    by simp
+  also have "-y = y"
+    by (rule uminus_CHAR_2) fact
+  finally show ?thesis .
+qed
+
+lemma (in semiring_1_cancel) of_nat_eq_iff_char_dvd:
+  assumes "m < n"
+  shows   "of_nat m = (of_nat n :: 'a) \<longleftrightarrow> CHAR('a) dvd (n - m)"
+proof
+  assume *: "of_nat m = (of_nat n :: 'a)"
+  have "of_nat n = (of_nat m + of_nat (n - m) :: 'a)"
+    using assms by (metis le_add_diff_inverse local.of_nat_add nless_le)
+  hence "of_nat (n - m) = (0 :: 'a)"
+    by (simp add: *)
+  thus "CHAR('a) dvd (n - m)"
+    by (simp add: of_nat_eq_0_iff_char_dvd)
+next
+  assume "CHAR('a) dvd (n - m)"
+  hence "of_nat (n - m) = (0 :: 'a)"
+    by (simp add: of_nat_eq_0_iff_char_dvd)
+  hence "of_nat m = (of_nat m + of_nat (n - m) :: 'a)"
+    by simp
+  also have "\<dots> = of_nat n"
+    using assms by (metis le_add_diff_inverse local.of_nat_add nless_le)
+  finally show "of_nat m = (of_nat n :: 'a)" .
+qed
+
+lemma (in ring_1) of_int_eq_0_iff_char_dvd:
+  "(of_int n = (0 :: 'a)) = (int CHAR('a) dvd n)"
+proof (cases "n \<ge> 0")
+  case True
+  hence "(of_int n = (0 :: 'a)) \<longleftrightarrow> (of_nat (nat n)) = (0 :: 'a)"
+    by auto
+  also have "\<dots> \<longleftrightarrow> CHAR('a) dvd nat n"
+    by (subst of_nat_eq_0_iff_char_dvd) auto
+  also have "\<dots> \<longleftrightarrow> int CHAR('a) dvd n"
+    using True by presburger
+  finally show ?thesis .
+next
+  case False
+  hence "(of_int n = (0 :: 'a)) \<longleftrightarrow> -(of_nat (nat (-n))) = (0 :: 'a)"
+    by auto
+  also have "\<dots> \<longleftrightarrow> CHAR('a) dvd nat (-n)"
+    by (auto simp: of_nat_eq_0_iff_char_dvd)
+  also have "\<dots> \<longleftrightarrow> int CHAR('a) dvd n"
+    using False dvd_nat_abs_iff[of "CHAR('a)" n] by simp
+  finally show ?thesis .
+qed
+
+lemma (in semiring_1_cancel) finite_imp_CHAR_pos:
+  assumes "finite (UNIV :: 'a set)"
+  shows   "CHAR('a) > 0"
+proof -
+  have "\<exists>n\<in>UNIV. infinite {m \<in> UNIV. of_nat m = (of_nat n :: 'a)}"
+  proof (rule pigeonhole_infinite)
+    show "infinite (UNIV :: nat set)"
+      by simp
+    show "finite (range (of_nat :: nat \<Rightarrow> 'a))"
+      by (rule finite_subset[OF _ assms]) auto
+  qed
+  then obtain n :: nat where "infinite {m \<in> UNIV. of_nat m = (of_nat n :: 'a)}"
+    by blast
+  hence "\<not>({m \<in> UNIV. of_nat m = (of_nat n :: 'a)} \<subseteq> {n})"
+    by (intro notI) (use finite_subset in blast)
+  then obtain m where "m \<noteq> n" "of_nat m = (of_nat n :: 'a)"
+    by blast
+  thus ?thesis
+  proof (induction m n rule: linorder_wlog)
+    case (le m n)
+    hence "CHAR('a) dvd (n - m)"
+      using of_nat_eq_iff_char_dvd[of m n] by auto
+    thus ?thesis
+      using le by (intro Nat.gr0I) auto
+  qed (simp_all add: eq_commute)
+qed
+
 end

--- a/src/HOL/Number_Theory/Cong.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -747,4 +747,29 @@
     by blast
 qed
 
+lemma (in semiring_1_cancel) of_nat_eq_iff_cong_CHAR:
+  "of_nat x = (of_nat y :: 'a) \<longleftrightarrow> [x = y] (mod CHAR('a))"
+proof (induction x y rule: linorder_wlog)
+  case (le x y)
+  define z where "z = y - x"
+  have [simp]: "y = x + z"
+    using le by (auto simp: z_def)
+  have "(CHAR('a) dvd z) = [x = x + z] (mod CHAR('a))"
+    by (metis \<open>y = x + z\<close> cong_def le mod_eq_dvd_iff_nat z_def)
+  thus ?case
+    by (simp add: of_nat_eq_0_iff_char_dvd)
+qed (simp add: eq_commute cong_sym_eq)   
+
+lemma (in ring_1) of_int_eq_iff_cong_CHAR:
+  "of_int x = (of_int y :: 'a) \<longleftrightarrow> [x = y] (mod int CHAR('a))"
+proof -
+  have "of_int x = (of_int y :: 'a) \<longleftrightarrow> of_int (x - y) = (0 :: 'a)"
+    by auto
+  also have "\<dots> \<longleftrightarrow> (int CHAR('a) dvd x - y)"
+    by (rule of_int_eq_0_iff_char_dvd)
+  also have "\<dots> \<longleftrightarrow> [x = y] (mod int CHAR('a))"
+    by (simp add: cong_iff_dvd_diff)
+  finally show ?thesis .
+qed
+
 end

--- a/src/HOL/Number_Theory/Residues.thy	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Thu Apr 04 15:29:41 2024 +0200
@@ -14,6 +14,66 @@
   Totient
 begin
 
+lemma (in ring_1) CHAR_dvd_CARD: "CHAR('a) dvd card (UNIV :: 'a set)"
+proof (cases "card (UNIV :: 'a set) = 0")
+  case False
+  hence [intro]: "CHAR('a) > 0"
+    by (simp add: card_eq_0_iff finite_imp_CHAR_pos)    
+  define G where "G = \<lparr> carrier = (UNIV :: 'a set), monoid.mult = (+), one = (0 :: 'a) \<rparr>"
+  define H where "H = (of_nat ` {..<CHAR('a)} :: 'a set)"
+  interpret group G
+  proof (rule groupI)
+    fix x assume x: "x \<in> carrier G"
+    show "\<exists>y\<in>carrier G. y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>"
+      by (intro bexI[of _ "-x"]) (auto simp: G_def)
+  qed (auto simp: G_def add_ac)
+
+  interpret subgroup H G
+  proof
+    show "\<one>\<^bsub>G\<^esub> \<in> H"
+      using False unfolding G_def H_def by force
+  next
+    fix x y :: 'a
+    assume "x \<in> H" "y \<in> H"
+    then obtain x' y' where [simp]: "x = of_nat x'" "y = of_nat y'"
+      by (auto simp: H_def)
+    have "x + y = of_nat ((x' + y') mod CHAR('a))"
+      by (auto simp flip: of_nat_add simp: of_nat_eq_iff_cong_CHAR)
+    moreover have "(x' + y') mod CHAR('a) < CHAR('a)"
+      using H_def \<open>y \<in> H\<close> by fastforce
+    ultimately show "x \<otimes>\<^bsub>G\<^esub> y \<in> H"
+      by (auto simp: H_def G_def intro!: imageI)
+  next
+    fix x :: 'a
+    assume x: "x \<in> H"
+    then obtain x' where [simp]: "x = of_nat x'" and x': "x' < CHAR('a)"
+      by (auto simp: H_def)
+    have "CHAR('a) dvd x' + (CHAR('a) - x') mod CHAR('a)"
+      using mod_eq_0_iff_dvd mod_if x' by fastforce
+    hence "x + of_nat ((CHAR('a) - x') mod CHAR('a)) = 0"
+      by (auto simp flip: of_nat_add simp: of_nat_eq_0_iff_char_dvd)
+    moreover from this have "inv\<^bsub>G\<^esub> x = of_nat ((CHAR('a) - x') mod CHAR('a))"
+      by (intro inv_equality) (auto simp: G_def add_ac)
+    moreover have "of_nat ((CHAR('a) - x') mod CHAR('a)) \<in> H"
+      unfolding H_def using \<open>CHAR('a) > 0\<close> by (intro imageI) auto
+    ultimately show "inv\<^bsub>G\<^esub> x \<in> H" by force
+  qed (auto simp: G_def H_def)
+
+  have "card H dvd card (rcosets\<^bsub>G\<^esub> H) * card H"
+    by simp
+  also have "card (rcosets\<^bsub>G\<^esub> H) * card H = Coset.order G"
+  proof (rule lagrange_finite)
+    show "finite (carrier G)"
+      using False card_ge_0_finite by (auto simp: G_def)
+  qed (fact is_subgroup)
+  finally have "card H dvd card (UNIV :: 'a set)"
+    by (simp add: Coset.order_def G_def)
+  also have "card H = card {..<CHAR('a)}"
+    unfolding H_def by (intro card_image inj_onI) (auto simp: of_nat_eq_iff_cong_CHAR cong_def)
+  finally show "CHAR('a) dvd card (UNIV :: 'a set)"
+    by simp
+qed auto
+
 definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool"
   where "QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))"
 

--- a/src/HOL/ROOT	Thu Apr 04 11:40:45 2024 +0200
+++ b/src/HOL/ROOT	Thu Apr 04 15:29:41 2024 +0200
@@ -436,6 +436,7 @@
     Divisibility         (* Rings *)
     IntRing              (* Ideals and residue classes *)
     UnivPoly             (* Polynomials *)
+    Algebraic_Closure_Type
     (* Main theory *)
     Algebra
   document_files "root.bib" "root.tex"