diff --git a/metadata/entries/Finite_Fields.toml b/metadata/entries/Finite_Fields.toml
--- a/metadata/entries/Finite_Fields.toml
+++ b/metadata/entries/Finite_Fields.toml
@@ -1,37 +1,39 @@
title = "Finite Fields"
date = 2022-06-08
topics = [
"Mathematics/Algebra",
]
abstract = """
This entry formalizes the classification of the finite fields (also
called Galois fields): For each prime power $p^n$ there exists exactly
one (up to isomorphisms) finite field of that size and there are no
other finite fields. The derivation includes a formalization of the
-characteristic of rings, the Frobenius endomorphism, formal
-differentiation for polynomials in HOL-Algebra and Gauss' formula
-for the number of monic irreducible polynomials over finite fields: \\[
+characteristic of rings, the Frobenius endomorphism, formal differentiation
+for polynomials in HOL-Algebra, Rabin's test for the irreducibility of
+polynomials and Gauss' formula for the number of monic irreducible
+polynomials over finite fields: \\[
\\frac{1}{n} \\sum_{d | n} \\mu(d) p^{n/d} \\textrm{.} \\] The proofs are
-based on the books from Ireland
-and Rosen, as well as, Lidl and
+and Rosen, Rabin, as
+well as, Lidl and
Niederreiter."""
license = "bsd"
note = ""
[authors]
[authors.karayel]
homepage = "karayel_homepage"
[contributors]
[notify]
karayel = "karayel_email"
[history]
+2023-01-17 = "Added Rabin's test for the irreducibility of polynomials in finite fields."
[extra]
[related]
diff --git a/thys/Finite_Fields/ROOT b/thys/Finite_Fields/ROOT
--- a/thys/Finite_Fields/ROOT
+++ b/thys/Finite_Fields/ROOT
@@ -1,18 +1,19 @@
chapter AFP
session Finite_Fields = "HOL-Algebra" +
options [timeout = 600]
sessions
Dirichlet_Series
theories
Card_Irreducible_Polynomials
Card_Irreducible_Polynomials_Aux
Finite_Fields_Factorization_Ext
Finite_Fields_Isomorphic
Finite_Fields_Preliminary_Results
Formal_Polynomial_Derivatives
Monic_Polynomial_Factorization
Ring_Characteristic
+ Rabin_Irreducibility_Test
document_files
"root.tex"
"root.bib"
diff --git a/thys/Finite_Fields/Rabin_Irreducibility_Test.thy b/thys/Finite_Fields/Rabin_Irreducibility_Test.thy
new file mode 100644
--- /dev/null
+++ b/thys/Finite_Fields/Rabin_Irreducibility_Test.thy
@@ -0,0 +1,371 @@
+section \Rabin's test for irreducible polynomials\
+
+theory Rabin_Irreducibility_Test
+ imports Card_Irreducible_Polynomials_Aux
+begin
+
+text \This section introduces an effective test for irreducibility of polynomials
+(in finite fields) based on Rabin~\cite[rabin1980].\
+
+lemma (in domain) coeff_a_inv:
+ assumes "subring K R"
+ assumes "f \ carrier (K[X])"
+ shows "coeff (\\<^bsub>K[X]\<^esub> f) i = \ (coeff f i)" (is "?L = ?R")
+proof -
+ have "?L = coeff (map (a_inv R) f) i"
+ unfolding univ_poly_a_inv_def'[OF assms(1,2)] by simp
+ also have "... = ?R" by (induction f) auto
+ finally show ?thesis by simp
+qed
+
+lemma (in comm_monoid) irreducible_prod_unit:
+ assumes "f \ carrier G" "x \ Units G"
+ shows "irreducible G f = irreducible G (x \ f)" (is "?L = ?R")
+proof
+ assume "?L"
+ thus ?R using irreducible_prod_lI assms by auto
+next
+ have "inv x \ (x \ f) = (inv x \ x) \ f"
+ using assms by (intro m_assoc[symmetric]) auto
+ also have "... = f" using assms by simp
+ finally have 0: "inv x \ (x \ f) = f" by simp
+ assume ?R
+ hence "irreducible G (inv x \ (x \ f) )" using irreducible_prod_lI assms by blast
+ thus ?L using 0 by simp
+qed
+
+definition pcoprime :: "_ \ 'a list \ 'a list \ bool" ("pcoprime\")
+ where "pcoprime\<^bsub>R\<^esub> p q =
+ (\r \ carrier (poly_ring R). r pdivides\<^bsub>R\<^esub> p \ r pdivides\<^bsub>R\<^esub> q \ degree r = 0)"
+
+lemma pcoprimeI:
+ assumes "\r. r \ carrier (poly_ring R) \ r pdivides \<^bsub>R\<^esub> p \ r pdivides\<^bsub>R\<^esub> q \ degree r = 0"
+ shows "pcoprime\<^bsub>R\<^esub> p q"
+ using assms unfolding pcoprime_def by auto
+
+context field
+begin
+
+interpretation r:polynomial_ring R "(carrier R)"
+ unfolding polynomial_ring_def polynomial_ring_axioms_def
+ using carrier_is_subfield field_axioms by force
+
+lemma pcoprime_one: "pcoprime\<^bsub>R\<^esub> p \\<^bsub>poly_ring R\<^esub>"
+proof (rule pcoprimeI)
+ fix r
+ assume r_carr: "r \ carrier (poly_ring R)"
+ moreover assume "r pdivides \<^bsub>R\<^esub> \\<^bsub>poly_ring R\<^esub>"
+ moreover have "\\<^bsub>poly_ring R\<^esub> \ []" by (simp add:univ_poly_one)
+ ultimately have "degree r \ degree \\<^bsub>poly_ring R\<^esub>"
+ by (intro pdivides_imp_degree_le[OF carrier_is_subring] r_carr) auto
+ also have "... = 0" by (simp add:univ_poly_one)
+ finally show "degree r = 0" by auto
+qed
+
+lemma pcoprime_left_factor:
+ assumes "x \ carrier (poly_ring R)"
+ assumes "y \ carrier (poly_ring R)"
+ assumes "z \ carrier (poly_ring R)"
+ assumes "pcoprime\<^bsub>R\<^esub> (x \\<^bsub>poly_ring R\<^esub> y) z"
+ shows "pcoprime\<^bsub>R\<^esub> x z"
+proof (rule pcoprimeI)
+ fix r
+ assume r_carr: "r \ carrier (poly_ring R)"
+ assume "r pdivides \<^bsub>R\<^esub> x"
+ hence "r pdivides \<^bsub>R\<^esub> (x \\<^bsub>poly_ring R\<^esub> y)"
+ using assms(1,2) r_carr r.p.divides_prod_r unfolding pdivides_def by simp
+ moreover assume "r pdivides \<^bsub>R\<^esub> z"
+ ultimately show "degree r = 0" using assms(4) r_carr unfolding pcoprime_def by simp
+qed
+
+lemma pcoprime_sym:
+ shows "pcoprime x y = pcoprime y x"
+ unfolding pcoprime_def by auto
+
+lemma pcoprime_left_assoc_cong_aux:
+ assumes "x1 \ carrier (poly_ring R)" "x2 \ carrier (poly_ring R)"
+ assumes "x2 \\<^bsub>poly_ring R\<^esub> x1"
+ assumes "y \ carrier (poly_ring R)"
+ assumes "pcoprime x1 y"
+ shows "pcoprime x2 y"
+ using assms r.p.divides_cong_r[OF _ assms(3)] unfolding pcoprime_def pdivides_def by simp
+
+lemma pcoprime_left_assoc_cong:
+ assumes "x1 \ carrier (poly_ring R)" "x2 \ carrier (poly_ring R)"
+ assumes "x1 \\<^bsub>poly_ring R\<^esub> x2"
+ assumes "y \ carrier (poly_ring R)"
+ shows "pcoprime x1 y = pcoprime x2 y"
+ using assms pcoprime_left_assoc_cong_aux r.p.associated_sym by metis
+
+lemma pcoprime_right_assoc_cong:
+ assumes "x1 \ carrier (poly_ring R)" "x2 \ carrier (poly_ring R)"
+ assumes "x1 \\<^bsub>poly_ring R\<^esub> x2"
+ assumes "y \ carrier (poly_ring R)"
+ shows "pcoprime y x1 = pcoprime y x2"
+ using assms pcoprime_sym pcoprime_left_assoc_cong by metis
+
+lemma pcoprime_step:
+ assumes "f \ carrier (poly_ring R)"
+ assumes "g \ carrier (poly_ring R)"
+ shows "pcoprime f g \ pcoprime g (f pmod g)"
+proof -
+ have "d pdivides f \ d pdivides (f pmod g)" if "d \ carrier (poly_ring R)" "d pdivides g" for d
+ proof -
+ have "d pdivides f \ d pdivides (g \\<^bsub>r.P\<^esub> (f pdiv g) \\<^bsub>r.P\<^esub> (f pmod g))"
+ using pdiv_pmod[OF carrier_is_subfield assms] by simp
+ also have "... \ d pdivides ((f pmod g))"
+ using that assms long_division_closed[OF carrier_is_subfield] r.p.divides_prod_r
+ unfolding pdivides_def by (intro r.p.div_sum_iff) simp_all
+ finally show ?thesis by simp
+ qed
+ hence "d pdivides f \ d pdivides g \ d pdivides g \ d pdivides (f pmod g)"
+ if "d \ carrier (poly_ring R)" for d
+ using that by auto
+ thus ?thesis
+ unfolding pcoprime_def by auto
+qed
+
+lemma pcoprime_zero_iff:
+ assumes "f \ carrier (poly_ring R)"
+ shows "pcoprime f [] \ length f = 1"
+proof -
+ consider (i) "length f = 0" | (ii) "length f = 1" | (iii) "length f > 1"
+ by linarith
+ thus ?thesis
+ proof (cases)
+ case i
+ hence "f = []" by simp
+ moreover have "X pdivides []" using r.pdivides_zero r.var_closed(1) by blast
+ moreover have "degree X = 1" using degree_var by simp
+ ultimately have "\pcoprime f []" using r.var_closed(1) unfolding pcoprime_def by auto
+ then show ?thesis using i by auto
+ next
+ case ii
+ hence "f \ []" "degree f = 0" by auto
+ hence "degree d = 0" if "d pdivides f" "d \ carrier (poly_ring R)" for d
+ using that(1) pdivides_imp_degree_le[OF carrier_is_subring that(2) assms] by simp
+ hence "pcoprime f []" unfolding pcoprime_def by auto
+ then show ?thesis using ii by simp
+ next
+ case iii
+ have "f pdivides f" using assms unfolding pdivides_def by simp
+ moreover have "f pdivides []" using assms r.pdivides_zero by blast
+ moreover have "degree f > 0" using iii by simp
+ ultimately have "\pcoprime f []" using assms unfolding pcoprime_def by auto
+ then show ?thesis using iii by auto
+ qed
+qed
+
+end
+
+context finite_field
+begin
+
+interpretation r:polynomial_ring R "(carrier R)"
+ unfolding polynomial_ring_def polynomial_ring_axioms_def
+ using carrier_is_subfield field_axioms by force
+
+lemma exists_irreducible_proper_factor:
+ assumes "monic_poly R f" "degree f > 0" "\monic_irreducible_poly R f"
+ shows "\g. monic_irreducible_poly R g \ g pdivides\<^bsub>R\<^esub> f \ degree g < degree f"
+proof -
+ define S where "S = {d. monic_irreducible_poly R d \ 0 < pmult d f}"
+
+ have f_carr: "f \ carrier (poly_ring R)" "f \ \\<^bsub>poly_ring R\<^esub>"
+ using assms(1) unfolding monic_poly_def univ_poly_zero by auto
+
+ have "S \ {}"
+ proof (rule ccontr)
+ assume S_empty: "\(S \ {})"
+ have "f = (\\<^bsub>poly_ring R\<^esub>d\S. d [^]\<^bsub>poly_ring R\<^esub> pmult d f)"
+ unfolding S_def by (intro factor_monic_poly assms(1))
+ also have "... = \\<^bsub>poly_ring R\<^esub>" using S_empty by simp
+ finally have "f = \\<^bsub>poly_ring R\<^esub>" by simp
+ hence "degree f = 0" using degree_one by simp
+ thus "False" using assms(2) by simp
+ qed
+ then obtain g where g_irred: "monic_irreducible_poly R g" and "0 < pmult g f"
+ unfolding S_def by auto
+
+ hence "1 \ pmult g f" by simp
+
+ hence g_div: "g pdivides f" using multiplicity_ge_1_iff_pdivides f_carr g_irred by blast
+
+ then obtain h where f_def: "f = g \\<^bsub>poly_ring R\<^esub> h" and h_carr:"h \ carrier (poly_ring R)"
+ unfolding pdivides_def by auto
+
+ have g_nz: "g \ \\<^bsub>poly_ring R\<^esub>" and h_nz: "h \ \\<^bsub>poly_ring R\<^esub>"
+ and g_carr: "g \ carrier (poly_ring R)"
+ using f_carr(2) h_carr g_irred unfolding f_def monic_irreducible_poly_def monic_poly_def
+ by auto
+
+ have "degree f = degree g + degree h"
+ using g_nz h_nz g_carr h_carr unfolding f_def by (intro degree_mult[OF r.K_subring]) auto
+ moreover have "degree h > 0"
+ proof (rule ccontr)
+ assume "\(degree h > 0)"
+ hence "degree h = 0" by simp
+ hence "h \ Units (poly_ring R)"
+ using h_carr h_nz by (simp add: carrier_is_subfield univ_poly_units' univ_poly_zero)
+ hence "f \\<^bsub>poly_ring R\<^esub> g"
+ unfolding f_def using g_carr r.p.associatedI2' by force
+ hence "f \\<^bsub>mult_of (poly_ring R)\<^esub> g"
+ using f_carr g_nz g_carr by (simp add: r.p.assoc_iff_assoc_mult)
+ hence "f = g"
+ using monic_poly_not_assoc assms(1) g_irred unfolding monic_irreducible_poly_def by simp
+ hence "monic_irreducible_poly R f"
+ using g_irred by simp
+ thus "False"
+ using assms(3) by auto
+ qed
+ ultimately have "degree g < degree f" by simp
+ thus ?thesis using g_irred g_div by auto
+qed
+
+theorem rabin_irreducibility_condition:
+ assumes "monic_poly R f" "degree f > 0"
+ defines "N \ {degree f div p | p . Factorial_Ring.prime p \ p dvd degree f}"
+ shows "monic_irreducible_poly R f \
+ (f pdivides gauss_poly R (order R^degree f) \ (\n \ N. pcoprime (gauss_poly R (order R^n)) f))"
+ (is "?L \ ?R1 \ ?R2")
+proof -
+ have f_carr: "f \ carrier (poly_ring R)"
+ using assms(1) unfolding monic_poly_def by blast
+
+ have "?R1" if "?L"
+ using div_gauss_poly_iff[where n="degree f"] that assms(2) by simp
+ moreover have "False" if cthat:"\pcoprime (gauss_poly R (order R^n)) f" "?L" "n \ N" for n
+ proof -
+ obtain d where d_def:
+ "d pdivides f"
+ "d pdivides (gauss_poly R (order R^n))" "degree d > 0" "d \ carrier (poly_ring R)"
+ using cthat(1) unfolding pcoprime_def by auto
+
+ obtain p where p_def:
+ "n = degree f div p" "Factorial_Ring.prime p" "p dvd degree f"
+ using cthat(3) unfolding N_def by auto
+
+ have n_gt_0: "n > 0"
+ using p_def assms(2) by (metis dvd_div_eq_0_iff gr0I)
+
+ have "d \ Units (poly_ring R)"
+ using d_def(3,4) univ_poly_units'[OF carrier_is_subfield] by simp
+ hence "f pdivides d"
+ using cthat(2) d_def(1,4) unfolding monic_irreducible_poly_def ring_irreducible_def
+ Divisibility.irreducible_def properfactor_def pdivides_def f_carr by auto
+ hence "f pdivides (gauss_poly R (order R^n))"
+ using d_def(2,4) f_carr r.p.divides_trans unfolding pdivides_def by metis
+ hence "degree f dvd n"
+ using n_gt_0 div_gauss_poly_iff[OF _ cthat(2)] by auto
+ thus "False"
+ using p_def by (metis assms(2) div_less_dividend n_gt_0 nat_dvd_not_less prime_gt_1_nat)
+ qed
+ moreover have "False" if not_l:"\?L" and r1:"?R1" and r2: "?R2"
+ proof -
+ obtain g where g_def: "g pdivides f" "degree g < degree f" "monic_irreducible_poly R g"
+ using r1 not_l exists_irreducible_proper_factor assms(1,2) by auto
+
+ have g_carr: "g \ carrier (poly_ring R)" and g_nz: "g \ \\<^bsub>poly_ring R\<^esub>"
+ using g_def(3) unfolding monic_irreducible_poly_def monic_poly_def by (auto simp:univ_poly_zero)
+
+ have "g pdivides gauss_poly R (order R^degree f)"
+ using g_carr r1 g_def(1) unfolding pdivides_def using r.p.divides_trans by blast
+
+ hence "degree g dvd degree f"
+ using div_gauss_poly_iff[OF assms(2) g_def(3)] by auto
+
+ then obtain t where deg_f_def:"degree f = t * degree g"
+ by fastforce
+ hence "t > 1" using g_def(2) by simp
+ then obtain p where p_prime: "Factorial_Ring.prime p" "p dvd t"
+ by (metis order_less_irrefl prime_factor_nat)
+ hence p_div_deg_f: "p dvd degree f"
+ unfolding deg_f_def by simp
+ define n where "n = degree f div p"
+ have n_in_N: "n \ N"
+ unfolding N_def n_def using p_prime(1) p_div_deg_f by auto
+
+ have deg_g_dvd_n: "degree g dvd n"
+ using p_prime(2) unfolding n_def deg_f_def by auto
+
+ have n_gt_0: "n > 0"
+ using p_div_deg_f assms(2) p_prime(1) unfolding n_def
+ by (metis dvd_div_eq_0_iff gr0I)
+
+ have deg_g_gt_0: "degree g > 0"
+ using monic_poly_min_degree[OF g_def(3)] by simp
+
+ have 0:"g pdivides gauss_poly R (order R^n)"
+ using deg_g_dvd_n div_gauss_poly_iff[OF n_gt_0 g_def(3)] by simp
+
+ have "pcoprime (gauss_poly R (order R^n)) f"
+ using n_in_N r2 by simp
+ thus "False"
+ using 0 g_def(1) g_carr deg_g_gt_0 unfolding pcoprime_def by simp
+ qed
+ ultimately show ?thesis
+ by auto
+qed
+
+text \A more general variance of the previous theorem for non-monic polynomials. The result is
+from Lemma~1 \cite[rabin1980].\
+
+theorem rabin_irreducibility_condition_2:
+ assumes "f \ carrier (poly_ring R)" "degree f > 0"
+ defines "N \ {degree f div p | p . Factorial_Ring.prime p \ p dvd degree f}"
+ shows "pirreducible (carrier R) f \
+ (f pdivides gauss_poly R (order R^degree f) \ (\n \ N. pcoprime (gauss_poly R (order R^n)) f))"
+ (is "?L \ ?R1 \ ?R2")
+proof -
+ define \ where "\ = [inv (hd f)]"
+ let ?g = "(\x. gauss_poly R (order R^x))"
+ let ?h = "\ \\<^bsub>poly_ring R\<^esub> f"
+
+ have f_nz: "f \ \\<^bsub>poly_ring R\<^esub>" unfolding univ_poly_zero using assms(2) by auto
+
+ hence "hd f \ carrier R - {\}" using assms(1) lead_coeff_carr by simp
+ hence "inv (hd f) \ carrier R - {\}" using field_Units by auto
+ hence \_unit: "\ \ Units (poly_ring R)"
+ unfolding \_def using univ_poly_carrier_units by simp
+
+ have \_nz: "\ \ \\<^bsub>poly_ring R\<^esub>" unfolding univ_poly_zero \_def by simp
+ have "hd ?h = hd \ \ hd f"
+ using \_nz f_nz assms(1) \_unit by (intro lead_coeff_mult) auto
+ also have "... = inv (hd f) \ hd f" unfolding \_def by simp
+ also have "... = \" using lead_coeff_carr f_nz assms(1) by (simp add: field_Units)
+ finally have "hd ?h = \" by simp
+ moreover have "?h \ []"
+ using \_nz f_nz univ_poly_zero by (metis \_unit assms(1) r.p.Units_closed r.p.integral)
+ ultimately have h_monic: "monic_poly R ?h"
+ using r.p.Units_closed[OF \_unit] assms(1) unfolding monic_poly_def by auto
+
+ have "degree ?h = degree \ + degree f"
+ using assms(1) f_nz \_unit \_nz by (intro degree_mult[OF carrier_is_subring]) auto
+ also have "... = degree f" unfolding \_def by simp
+ finally have deg_f: "degree f = degree ?h" by simp
+
+ have hf_cong:"?h \\<^bsub>r.P\<^esub> f"
+ using assms(1) \_unit by (simp add: r.p.Units_closed r.p.associatedI2 r.p.m_comm)
+ hence 0: "f pdivides ?g (degree f) \ ?h pdivides ?g (degree f)"
+ unfolding pdivides_def using r.p.divides_cong_l r.p.associated_sym
+ using r.p.Units_closed[OF \_unit] assms(1) gauss_poly_carr by blast
+
+ have 1: "pcoprime (?g n) f \ pcoprime (?g n) ?h" for n
+ using hf_cong r.p.associated_sym r.p.Units_closed[OF \_unit] assms(1)
+ by (intro pcoprime_right_assoc_cong gauss_poly_carr) auto
+
+ have "?L \ pirreducible (carrier R) (\ \\<^bsub>poly_ring R\<^esub> f)"
+ using \_unit \_nz assms(1) f_nz r.p.integral unfolding ring_irreducible_def
+ by (intro arg_cong2[where f="(\)"] r.p.irreducible_prod_unit assms) auto
+ also have "... \ monic_irreducible_poly R (\ \\<^bsub>poly_ring R\<^esub> f)"
+ using h_monic unfolding monic_irreducible_poly_def by auto
+ also have "... \ ?h pdivides ?g (degree f) \ (\n \ N. pcoprime (?g n) ?h)"
+ using assms(2) unfolding N_def deg_f by (intro rabin_irreducibility_condition h_monic) auto
+ also have "... \ f pdivides ?g (degree f) \ (\n \ N. pcoprime (?g n) f)"
+ using 0 1 by simp
+ finally show ?thesis by simp
+qed
+
+end
+
+end
\ No newline at end of file
diff --git a/thys/Finite_Fields/document/root.bib b/thys/Finite_Fields/document/root.bib
--- a/thys/Finite_Fields/document/root.bib
+++ b/thys/Finite_Fields/document/root.bib
@@ -1,42 +1,53 @@
@book{ireland1982,
author = {Kenneth Ireland and
Michael Rosen},
title = {A classical introduction to modern number theory},
series = {Graduate texts in mathematics},
volume = {84},
publisher = {Springer},
year = {1982},
isbn = {978-0-387-90625-6},
timestamp = {Fri, 28 Jun 2019 12:45:52 +0200},
biburl = {https://dblp.org/rec/books/daglib/0068082.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{lidl1986,
author = {Lidl, Rudolf and Niederreiter, Harald},
title = {Introduction to Finite Fields and Their Applications},
year = {1986},
isbn = {0521307066},
publisher = {Cambridge University Press},
address = {USA}
}
@article{chebolu2010,
title={Counting Irreducible Polynomials over Finite Fields Using the Inclusion-Exclusion Principle},
author={Sunil K. Chebolu and J{\'a}n Min{\'a}{\v{c}}},
journal={Mathematics Magazine},
year={2010},
volume={84},
pages={369 - 371}
}
@article{Dirichlet_Series-AFP,
author = {Manuel Eberl},
title = {Dirichlet Series},
journal = {Archive of Formal Proofs},
month = oct,
year = 2017,
note = {\url{https://isa-afp.org/entries/Dirichlet_Series.html},
Formal proof development},
ISSN = {2150-914x},
-}
\ No newline at end of file
+}
+
+@article{rabin1980,
+ author = {Rabin, Michael O.},
+ title = {Probabilistic Algorithms in Finite Fields},
+ journal = {SIAM Journal on Computing},
+ volume = {9},
+ number = {2},
+ pages = {273-280},
+ year = {1980},
+ doi = {10.1137/0209024},
+}
diff --git a/thys/Finite_Fields/document/root.tex b/thys/Finite_Fields/document/root.tex
--- a/thys/Finite_Fields/document/root.tex
+++ b/thys/Finite_Fields/document/root.tex
@@ -1,37 +1,37 @@
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage{pdfsetup}
\urlstyle{rm}
\isabellestyle{it}
\begin{document}
\title{Finite Fields}
\author{Emin Karayel}
\maketitle
\abstract{This entry formalizes the classification of the finite fields (also called Galois fields):
For each prime power $p^n$ there exists exactly one (up to isomorphisms) finite field of that size
and there are no other finite fields.
-The derivation includes a formalization of the characteristic of rings, the Frobenius endomorphism,
-formal differentiation for polynomials in HOL-Algebra and Gauss' formula for the number of
-monic irreducible polynomials over finite fields:
+The derivation includes a formalization of the characteristic of rings, the Frobenius endomorphism,
+formal differentiation for polynomials in HOL-Algebra, Rabin's test for the irreducibility of
+polynomials and Gauss' formula for the number of monic irreducible polynomials over finite fields:
\[
\frac{1}{n} \sum_{d | n} \mu(d) p^{n/d} \textrm{.}
\]
-The proofs are based on the books from Ireland and Rosen~\cite{ireland1982}, as well as,
-Lidl and Niederreiter~\cite{lidl1986}.
+The proofs are based on the books and publications from Ireland and Rosen~\cite{ireland1982}, Lidl
+and Niederreiter~\cite{lidl1986}, as well as, Rabin~\cite{rabin1980}.
}
-
+
\parindent 0pt\parskip 0.5ex
\tableofcontents
\input{session}
\bibliographystyle{abbrv}
\bibliography{root}
\end{document}
\ No newline at end of file