import Mathlib.FieldTheory.Finite.Basic
import Mathlib.FieldTheory.Finite.GaloisField
import Mathlib.Tactic

-- ============================================================================
-- GF(p): The Prime Field
-- ============================================================================
--
-- The simplest Galois fields are the prime fields GF(p) = ℤ/pℤ.
-- Arithmetic is just integers mod p.
--
-- Fundamental theorem: a finite field of order q exists iff q = p^n
-- for some prime p and n ≥ 1. So GF(2), GF(4), GF(8), GF(9) exist,
-- but GF(6) and GF(10) do not.
--
-- The prime field is the case n = 1: GF(p) = ℤ/pℤ.

-- ============================================================================
-- Section 1: GF(5) — a concrete prime field
-- ============================================================================

-- In Mathlib, ZMod p is already a field when p is prime.
-- Let's see it in action.

-- The elements of 𝔽₃ are {0, 1, 2}.
notation "𝔽₃" => ZMod 3

-- ## Property Clarification

-- ZMod n is always a commutative ring
instance : Ring 𝔽₃        := inferInstance
instance : CommRing 𝔽₃    := inferInstance

-- ZMod p is a finite field when p is prime
instance : Field 𝔽₃       := inferInstance
instance : Fintype 𝔽₃     := inferInstance

-- 𝔽₃ contains a multiplicative inverse for every nonzero element
instance : GroupWithZero 𝔽₃ := inferInstance
example (a : 𝔽₃) (ha : a ≠ 0) : a * a⁻¹ = 1 := mul_inv_cancel₀ ha

-- 𝔽₃ has no zero divisors
instance : NoZeroDivisors 𝔽₃ := inferInstance
example (a b : 𝔽₃) (h : a * b = 0) : a = 0 ∨ b = 0 := mul_eq_zero.mp h

-- The multiplicative group 𝔽₃ˣ (nonzero elements under multiplication) is
-- cyclic of order q-1 = 2
instance : IsCyclic 𝔽₃ˣ := inferInstance
example : Fintype.card 𝔽₃ˣ = 2 := by decide

-- 2 is a primitive element/root: its powers generate all nonzero elements
example : (2^1 : 𝔽₃) = 2 := by decide
example : (2^2 : 𝔽₃) = 1 := by decide

-- ============================================================================
-- Section 2: Characteristic — the prime "under the hood"
-- ============================================================================

-- The characteristic of a field is the smallest positive n such that
-- 1 + 1 + ... + 1 (n times) = 0. For GF(p), that's just p.

-- In 𝔽₃: 1 + 1 + 1 = 0, but no smaller sum works
example : (1 + 1 + 1 : 𝔽₃) = 0 := by decide -- eq

-- Mathlib knows the characteristic:
example : CharP (ZMod 5) 5 := ZMod.charP 5

-- ============================================================================
-- Section 3: Fermat's little theorem in GF(p)
-- ============================================================================
--
-- For any a in GF(p), a^p = a. This is a fundamental identity in finite fields.
example : (0 : 𝔽₃) ^ 3 = 0 := by decide
example : (1 : 𝔽₃) ^ 3 = 1 := by decide
example : (2 : 𝔽₃) ^ 3 = 2 := by decide

-- Equivalently, for nonzero a: a^(p-1) = 1.
example : (0 : 𝔽₃) ^ (3-1) = 0 := by decide
example : (1 : 𝔽₃) ^ (3-1) = 1 := by decide
example : (2 : 𝔽₃) ^ (3-1) = 1 := by decide

-- In any finite group, g^|G| = 1 (Lagrange). The nonzero elements form
-- 𝔽₃ˣ of order p-1 = 2
--
-- TODO: This should be in a dedicated `Group/` file.
example (g : 𝔽₃ˣ) : g ^ Fintype.card 𝔽₃ˣ = 1 := pow_card_eq_one

-- The general statement from Mathlib:
-- For any finite field of characteristic p, every element satisfies x^p = x.
--#check ZMod.pow_prime_eq (p := 5)

-- ============================================================================
-- Section 4: GF(p) has exactly p elements
-- ============================================================================

example : Fintype.card (ZMod 5) = 5 := by decide
example : Fintype.card (ZMod 2) = 2 := by decide
example : Fintype.card (ZMod 7) = 7 := by decide

-- ============================================================================
-- Section 5: Key Structural Theorems of Finite Fields
-- ============================================================================

-- 1. Uniqueness: all finite fields of the same order are isomorphic.
--    Given two finite fields K, K' over ZMod p with the same cardinality,
--    there is an algebra isomorphism between them.
#check @FiniteField.algEquivOfCardEq

-- 2. The multiplicative group of a finite field is cyclic.
--    i.e., the nonzero elements (units) under multiplication form a cyclic group.
--    For 𝔽₃, this means 𝔽₃ˣ ≅ ℤ/4ℤ, generated by some primitive root.
instance : IsCyclic 𝔽₃ˣ := inferInstance

-- 3. Subfield structure: GF(p^m) embeds into GF(p^n) iff m ∣ n.
--    Mathlib states this via algebra homomorphisms and finrank divisibility.
#check @FiniteField.nonempty_algHom_iff_finrank_dvd

-- 4. Frobenius automorphism: the map x ↦ x^p is a field automorphism.
--    Its powers generate the Galois group Gal(GF(p^n)/GF(p)) ≅ ℤ/nℤ.
#check @FiniteField.frobeniusAlgEquiv