@[reducible, inline]

abbrev 𝔽 (p : ℕ) : Type

Notation 𝔽 p for the finite field with p elements, defined as ZMod p (the quotient ℤ / p ℤ). Matches Definition 3.2.

def Fp (p : ℕ) : Type

Alternative non-abbrev synonym Fp p := ZMod p for 𝔽 p.

@[reducible, inline]

abbrev 𝔽q (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Type

Notation 𝔽q p n for the finite field with p^n elements, defined as GaloisField p n (the splitting field of X^(p^n) - X over 𝔽_p). Matches Definition 3.4.

theorem 𝔽q_isSplittingField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : Polynomial.IsSplittingField (ZMod p) (𝔽q p n) (Polynomial.X ^ p ^ n - Polynomial.X)

𝔽q p n is, by definition, the splitting field of X^(p^n) - X over 𝔽_p, matching the splitting-field description in Definition 3.4.

theorem 𝔽q_frobenius (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : n ≠ 0) (x : 𝔽q p n) : x ^ p ^ n = x

Frobenius identity in 𝔽q p n: every element satisfies x^(p^n) = x, i.e. 𝔽q p n consists of roots of X^(p^n) - X.

theorem 𝔽q_card (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : n ≠ 0) : Nat.card (𝔽q p n) = p ^ n

Theorem 3.6 (cardinality half): 𝔽q p n has exactly p^n elements.

noncomputable def 𝔽q_equivZModP (p : ℕ) [Fact (Nat.Prime p)] : 𝔽q p 1 ≃ₐ[ZMod p] ZMod p

𝔽q p 1 is canonically isomorphic to 𝔽_p = ZMod p as a ZMod p-algebra.

theorem 𝔽q_card_thm36 (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : n ≠ 0) : Nat.card (𝔽q p n) = p ^ n

Theorem 3.6, cardinality half: |𝔽q p n| = p^n.

noncomputable def 𝔽q_ringEquiv_of_card (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : n ≠ 0) (K : Type u_1) [Field K] [Fintype K] (hK : Fintype.card K = p ^ n) : K ≃+* 𝔽q p n

Theorem 3.6, uniqueness half (data form): a choice of ring isomorphism between any finite field K of cardinality p^n and 𝔽q p n.

theorem 𝔽q_unique_of_card (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : n ≠ 0) (K : Type u_1) [Field K] [Fintype K] (hK : Fintype.card K = p ^ n) : Nonempty (K ≃+* 𝔽q p n)

Theorem 3.6, uniqueness half (propositional form): any finite field of cardinality p^n is isomorphic to 𝔽q p n.

theorem Fq_unique_of_card (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) {K : Type u_1} [Field K] [Fintype K] (hn : n ≠ 0) (hcard : Fintype.card K = p ^ n) : Nonempty (K ≃+* 𝔽q p n)

Alias of 𝔽q_unique_of_card with implicit arguments restructured.

theorem finite_fields_isomorphic_of_card_eq (K₁ : Type u_1) (K₂ : Type u_2) [Field K₁] [Field K₂] [Fintype K₁] [Fintype K₂] (h : Fintype.card K₁ = Fintype.card K₂) : Nonempty (K₁ ≃+* K₂)

Two finite fields of the same cardinality are isomorphic — a general form of the uniqueness statement in Theorem 3.6.

theorem 𝔽q_subfield_iff (p : ℕ) [Fact (Nat.Prime p)] (m n : ℕ) (hm : m ≠ 0) (hn : n ≠ 0) : Nonempty (𝔽q p m →ₐ[ZMod p] 𝔽q p n) ↔ m ∣ n

Theorem 3.8: 𝔽_{p^m} embeds into 𝔽_{p^n} (as a ZMod p-algebra) iff m ∣ n.

@[implicit_reducible]

instance Fp_field (p : ℕ) [hp : Fact (Nat.Prime p)] : Field (𝔽 p)

𝔽 p is a field whenever p is prime.

theorem Fp_canonical_map (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [CharP K p] : ∃ (f : 𝔽 p →+* K), Function.Injective ⇑f

Theorem 3.3 (existence of canonical embedding): every field K of characteristic p admits a canonical injective ring homomorphism from 𝔽 p.

theorem Fp_unique_of_card (p : ℕ) (hp : Nat.Prime p) (K : Type u_1) [Field K] [Fintype K] (hK : Fintype.card K = p) : Nonempty (𝔽 p ≃+* K)

Theorem 3.3 (uniqueness): every field of cardinality p (with p prime) is isomorphic to 𝔽 p.

theorem fields_of_card_prime_isomorphic (p : ℕ) (hp : Nat.Prime p) (K₁ : Type u_1) (K₂ : Type u_2) [Field K₁] [Field K₂] [Fintype K₁] [Fintype K₂] (hK₁ : Fintype.card K₁ = p) (hK₂ : Fintype.card K₂ = p) : Nonempty (K₁ ≃+* K₂)

Two fields of prime cardinality p are isomorphic, by Theorem 3.3.

theorem char_p_contains_Fp (p : ℕ) [Fact (Nat.Prime p)] (K : Type u_1) [Field K] [CharP K p] : ∃ (f : 𝔽 p →+* K), Function.Injective ⇑f

Restatement of Fp_canonical_map: any field of characteristic p contains a copy of 𝔽 p via an injective ring homomorphism.

theorem Fp_unique_of_card_prime (p : ℕ) (hp : Nat.Prime p) (K : Type u_1) [Field K] [Fintype K] (hK : Fintype.card K = p) : Nonempty (𝔽 p ≃+* K)

Alias of Fp_unique_of_card: any field of prime cardinality p is isomorphic to 𝔽 p.

def Polynomial.IsSeparablePoly {k : Type u_1} [Field k] (f : Polynomial k) : Prop

Definition 3.17: f is separable iff it has deg f distinct roots in any algebraic closure — encoded here via Mathlib's Polynomial.Separable.

def Polynomial.IsInseparablePoly {k : Type u_1} [Field k] (f : Polynomial k) : Prop

A polynomial is inseparable iff it is not separable.

theorem Polynomial.isSeparablePoly_iff_separable {k : Type u_1} [Field k] (f : Polynomial k) : f.IsSeparablePoly ↔ f.Separable

Unfolding lemma: IsSeparablePoly f is definitionally f.Separable.

theorem Polynomial.isInseparablePoly_iff_not_separable {k : Type u_1} [Field k] (f : Polynomial k) : f.IsInseparablePoly ↔ ¬f.Separable

Unfolding lemma: IsInseparablePoly f is definitionally ¬ f.Separable.

theorem Polynomial.separable_iff_coprime_derivative {k : Type u_1} [Field k] (f : Polynomial k) : f.Separable ↔ IsCoprime f (derivative f)

One of the equivalent formulations from Definition 3.17: separability is the same as f being coprime to its derivative f'.

theorem Polynomial.separable_iff_card_rootSet_eq_natDegree {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {f : Polynomial k} (hf : f ≠ 0) (hsplit : (map (algebraMap k K) f).Splits) : f.Separable ↔ Fintype.card ↑(f.rootSet K) = f.natDegree

Definition 3.17, distinct-roots criterion: if f splits over K, then f is separable iff |{roots of f in K}| = deg f.

theorem Polynomial.separable_implies_squarefree {k : Type u_1} [Field k] {f : Polynomial k} (hsep : f.Separable) : Squarefree f

A separable polynomial is squarefree (one half of the squarefree-on-every- extension characterization in Definition 3.17).

theorem Polynomial.separable_iff_squarefree_of_perfectField {k : Type u_1} [Field k] [PerfectField k] (f : Polynomial k) : f.Separable ↔ Squarefree f

Over a perfect field, separability and squarefreeness coincide for polynomials.

theorem Polynomial.irreducible_inseparable_iff_derivative_eq_zero {k : Type u_1} [Field k] {f : Polynomial k} (hf : Irreducible f) : ¬f.Separable ↔ derivative f = 0

Lemma 3.20: an irreducible polynomial f is inseparable iff its formal derivative f' is identically zero.

theorem finite_mult_subgroup_of_field_isCyclic (k : Type u_1) [Field k] (G : Subgroup kˣ) [Finite ↥G] : IsCyclic ↥G

Theorem 3.12: every finite subgroup of the multiplicative group kˣ of a field is cyclic.

theorem finite_field_mult_isCyclic (k : Type u_1) [Field k] [Fintype k] : IsCyclic kˣ

Corollary 3.13: the multiplicative group kˣ of a finite field is cyclic.

instance 𝔽q_units_isCyclic (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : IsCyclic (𝔽q p n)ˣ

Specialization of Corollary 3.13 to 𝔽q p n: the multiplicative group (𝔽q p n)ˣ is cyclic.

def Polynomial.IsPrimitivePolynomial (p : ℕ) [Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) : Prop

Definition 3.14: a monic irreducible f ∈ 𝔽_p[x] is primitive iff its adjoined root has order p^(deg f) - 1 (i.e. generates the multiplicative group of 𝔽_p[x]/(f)).

theorem Polynomial.IsPrimitivePolynomial.monic (p : ℕ) [Fact (Nat.Prime p)] {f : Polynomial (ZMod p)} (hf : IsPrimitivePolynomial p f) : f.Monic

A primitive polynomial is monic.

theorem Polynomial.IsPrimitivePolynomial.irreducible (p : ℕ) [Fact (Nat.Prime p)] {f : Polynomial (ZMod p)} (hf : IsPrimitivePolynomial p f) : Irreducible f

A primitive polynomial is irreducible.

theorem Polynomial.IsPrimitivePolynomial.root_orderOf (p : ℕ) [Fact (Nat.Prime p)] {f : Polynomial (ZMod p)} (hf : IsPrimitivePolynomial p f) : orderOf (AdjoinRoot.root f) = p ^ f.natDegree - 1

For a primitive polynomial f, its adjoined root has order p^(deg f) - 1.

theorem perfectField_iff_irreducible_separable (k : Type u_1) [Field k] : PerfectField k ↔ ∀ (f : Polynomial k), Irreducible f → f.Separable

Equivalence: a field k is perfect (Definition 3.21) iff every irreducible polynomial in k[x] is separable.

theorem finite_field_isPerfect (K : Type u_1) [Field K] [Finite K] : PerfectField K

Theorem 3.22: every finite field is perfect.

noncomputable def quotient_irred_ringEquiv_𝔽q (p : ℕ) [hp : Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) [hf : Fact (Irreducible f)] (hn : f.natDegree ≠ 0) : AdjoinRoot f ≃+* 𝔽q p f.natDegree

Theorem 3.9 (data form): for any irreducible f ∈ 𝔽_p[x] of positive degree n, the quotient ring 𝔽_p[x]/(f) is ring-isomorphic to 𝔽_{p^n}.

theorem quotient_irred_iso_𝔽q (p : ℕ) [hp : Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) [hf : Fact (Irreducible f)] (hn : f.natDegree ≠ 0) : Nonempty (AdjoinRoot f ≃+* 𝔽q p f.natDegree)

Theorem 3.9 (propositional form): for irreducible f of positive degree, 𝔽_p[x]/(f) ≃ 𝔽_{p^{deg f}}.

theorem irred_splits_in_𝔽q (p : ℕ) [hp : Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) (hf : Irreducible f) (hn : f.natDegree ≠ 0) : (Polynomial.map (algebraMap (ZMod p) (𝔽q p f.natDegree)) f).Splits

Corollary 3.10: every irreducible f ∈ 𝔽_p[x] of positive degree n splits completely in 𝔽_{p^n}.

theorem Fq_irred_splits (p : ℕ) [hp : Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) (hf : Irreducible f) (hn : f.natDegree ≠ 0) : (Polynomial.map (algebraMap (ZMod p) (GaloisField p f.natDegree)) f).Splits

Restatement of Corollary 3.10 with GaloisField notation: irreducible f ∈ 𝔽_p[x] of positive degree n splits completely in GaloisField p n.

noncomputable def conwayCoeff (p : ℕ) [Fact (Nat.Prime p)] (f : Polynomial (ZMod p)) (i : ℕ) : ℕ

The i-th Conway coefficient of an order polynomial f from Definition 3.16: take (-1)^(deg f - i)·coeff_i(f) and reduce to a natural number in [0, p).

def conwayLT (p : ℕ) [Fact (Nat.Prime p)] (f g : Polynomial (ZMod p)) : Prop

The strict lexicographic order on Conway coefficients used to compare two order polynomials of the same degree, per Definition 3.16.

def ConwayCompatible (p : ℕ) [Fact (Nat.Prime p)] (fam : (m : ℕ) → 0 < m → Polynomial (ZMod p)) (n : ℕ) (f : Polynomial (ZMod p)) : Prop

Conway compatibility (Definition 3.16): for every proper divisor m ∣ n and every root α of fam m, f(α^(n/m)) = 0 holds in the algebraic closure of 𝔽_p.

structure IsConwayPolynomialSystem (p : ℕ) [Fact (Nat.Prime p)] (fam : (n : ℕ) → 0 < n → Polynomial (ZMod p)) : Prop

A family fam : ∀ n > 0, 𝔽_p[X] is a Conway polynomial system if it satisfies the recursive definition (Definition 3.16): the degree-one case is X - r for the least primitive root r; each higher polynomial is primitive, has the right degree, is compatible with smaller members, and is minimal under the Conway lex order among such primitives.

• degree_one : ∃ (r : ℕ), 0 < r ∧ r < p ∧ orderOf ↑r = p - 1 ∧ (∀ (s : ℕ), 0 < s → s < r → orderOf ↑s ≠ p - 1) ∧ fam 1 ⋯ = Polynomial.X - Polynomial.C ↑r
• isPrimitive (n : ℕ) (hn : 0 < n) : 1 < n → Polynomial.IsPrimitivePolynomial p (fam n hn)
• hasDegree (n : ℕ) (hn : 0 < n) : 1 < n → (fam n hn).natDegree = n
• compatible (n : ℕ) (hn : 0 < n) : 1 < n → ConwayCompatible p (fun (m : ℕ) (hm : 0 < m) => fam m hm) n (fam n hn)
• isLeast (n : ℕ) (hn : 0 < n) : 1 < n → ∀ (g : Polynomial (ZMod p)), Polynomial.IsPrimitivePolynomial p g → g.natDegree = n → ConwayCompatible p (fun (m : ℕ) (hm : 0 < m) => fam m hm) n g → ¬conwayLT p g (fam n hn)

theorem conwayPolynomialSystem_exists (p : ℕ) [Fact (Nat.Prime p)] : ∃ (fam : (n : ℕ) → 0 < n → Polynomial (ZMod p)), IsConwayPolynomialSystem p fam

Existence of a Conway polynomial system over 𝔽_p (Definition 3.16).

theorem orderOf_adjoinRoot_root_eq_orderOf (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] (α : E) (hint : IsIntegral F α) : orderOf (AdjoinRoot.root (minpoly F α)) = orderOf α

Auxiliary lemma for Theorem 3.15: for an integral element α of E/F, the order of AdjoinRoot.root (minpoly F α) equals orderOf α, via the ring isomorphism between F[x]/(minpoly α) and F(α).

theorem primitive_poly_exists (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : ∃ (f : Polynomial (ZMod p)), Polynomial.IsPrimitivePolynomial p f ∧ f.natDegree = n

Theorem 3.15 (existence half): for every prime p and positive n, there exists a primitive polynomial of degree n in 𝔽_p[x]. The construction takes the minimal polynomial of a generator of (𝔽_{p^n})ˣ.

theorem nat_card_eq_mul_of_const_fiber {A : Type u_1} {B : Type u_2} [Finite A] [Finite B] (f : A → B) (k : ℕ) (hfib : ∀ (b : B), Nat.card { a : A // f a = b } = k) : Nat.card A = k * Nat.card B

Generic counting lemma: if f : A → B has every fibre of cardinality k, then |A| = k · |B|. Used in counting primitive polynomials in Theorem 3.15.

theorem adjoin_top_of_unit_generator (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (g : (GaloisField p n)ˣ) (hg : orderOf g = p ^ n - 1) : (ZMod p)⟮↑g⟯ = ⊤

If g is a unit of 𝔽_{p^n} of order p^n - 1, then g generates the multiplicative group of 𝔽_{p^n} and 𝔽_p(g) = 𝔽_{p^n}.

theorem generator_minpoly_is_prim (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (g : (GaloisField p n)ˣ) (hg : orderOf g = p ^ n - 1) : have f := minpoly (ZMod p) ↑g; Polynomial.IsPrimitivePolynomial p f ∧ f.natDegree = n

If g is a generator of (𝔽_{p^n})ˣ, then its minimal polynomial over 𝔽_p is a primitive polynomial of degree n (cf. Theorem 3.15).

instance finite_primitivePolys (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : Finite { f : Polynomial (ZMod p) // Polynomial.IsPrimitivePolynomial p f ∧ f.natDegree = n }

The set of primitive polynomials of degree n in 𝔽_p[x] is finite: a primitive polynomial of degree n is determined by its n lower coefficients in 𝔽_p, of which there are finitely many.

theorem card_generators_eq_totient (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : Nat.card { g : (GaloisField p n)ˣ // orderOf g = p ^ n - 1 } = (p ^ n - 1).totient

In a cyclic group (𝔽_{p^n})ˣ of order p^n - 1, the number of generators is φ(p^n - 1) (Euler totient), the standard counting fact.

noncomputable def minpoly_of_generator (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (g : { g : (GaloisField p n)ˣ // orderOf g = p ^ n - 1 }) : { f : Polynomial (ZMod p) // Polynomial.IsPrimitivePolynomial p f ∧ f.natDegree = n }

The map from multiplicative generators of 𝔽_{p^n} to primitive polynomials of degree n, sending g to its minimal polynomial over 𝔽_p.

theorem minpoly_fiber_card (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) (f : { f : Polynomial (ZMod p) // Polynomial.IsPrimitivePolynomial p f ∧ f.natDegree = n }) : Nat.card { g : { g : (GaloisField p n)ˣ // orderOf g = p ^ n - 1 } // minpoly_of_generator p n hn g = f } = n

Each primitive polynomial of degree n is the minimal polynomial of exactly n generators of (𝔽_{p^n})ˣ (its n Galois conjugates).

theorem primitive_poly_count (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) (hn : 0 < n) : Nat.card { f : Polynomial (ZMod p) // Polynomial.IsPrimitivePolynomial p f ∧ f.natDegree = n } = (p ^ n - 1).totient / n

Theorem 3.15 (counting half): the number of primitive polynomials of degree n in 𝔽_p[x] is φ(p^n - 1) / n.