import Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
import Mathlib.Data.ZMod.Units
import Mathlib.Tactic

-- ============================================================================
-- Cyclic Groups
-- ============================================================================
--
-- A cyclic group is a group generated by a single element g.
-- Every element can be written as gⁿ for some integer n.
--
-- The cyclic group of order n is isomorphic to ℤ/nℤ (integers mod n).
-- These are the simplest possible groups.

-- ============================================================================
-- Section 1: ℤ/nℤ — the canonical cyclic group (additive)
-- ============================================================================

-- ℤ/4ℤ has 4 elements: {0, 1, 2, 3}
example : Fintype.card (ZMod 4) = 4 := by decide

-- It's a cyclic group (Mathlib uses Multiplicative wrapper for the group instance)
instance : IsCyclic (Multiplicative (ZMod 4)) := inferInstance

-- 1 generates everything by repeated addition:
-- 1, 1+1=2, 1+1+1=3, 1+1+1+1=0 (wraps back)
example : (1 + 1 : ZMod 4) = 2 := by decide
example : (1 + 1 + 1 : ZMod 4) = 3 := by decide
example : (1 + 1 + 1 + 1 : ZMod 4) = 0 := by decide

-- Addition is commutative (every cyclic group is abelian)
example : ∀ a b : ZMod 4, a + b = b + a := by decide

-- ============================================================================
-- Section 2: Multiplicative cyclic groups — units of 𝔽₅
-- ============================================================================

notation "𝔽₅" => ZMod 5
instance : Fact (Nat.Prime 5) := ⟨by norm_num⟩

-- 𝔽₅ˣ = {1, 2, 3, 4} under multiplication is cyclic of order 4
instance : IsCyclic 𝔽₅ˣ := inferInstance
example : Fintype.card 𝔽₅ˣ = 4 := by decide

-- 2 is a generator (primitive root): its powers exhaust all nonzero elements
example : (2 : 𝔽₅) ^ 1 = 2 := by decide
example : (2 : 𝔽₅) ^ 2 = 4 := by decide
example : (2 : 𝔽₅) ^ 3 = 3 := by decide  -- 8 mod 5 = 3
example : (2 : 𝔽₅) ^ 4 = 1 := by decide  -- 16 mod 5 = 1 (wraps back)

-- 3 is also a generator (φ(4) = 2 generators exist)
example : (3 : 𝔽₅) ^ 1 = 3 := by decide
example : (3 : 𝔽₅) ^ 2 = 4 := by decide
example : (3 : 𝔽₅) ^ 3 = 2 := by decide
example : (3 : 𝔽₅) ^ 4 = 1 := by decide

-- 4 is NOT a generator — it has order 2, not 4
example : (4 : 𝔽₅) ^ 2 = 1 := by decide  -- cycles back after just 2 steps

-- ============================================================================
-- Section 3: Key properties of cyclic groups
-- ============================================================================

-- Every subgroup of a cyclic group is cyclic
#check isCyclic_of_surjective

-- For a cyclic group of order n:
--   - It has exactly one subgroup of order d for each divisor d of n
--   - The number of generators equals Euler's totient φ(n)
--   - It is isomorphic to ℤ/nℤ

-- Example: ℤ/6ℤ has divisors {1, 2, 3, 6},
-- so it has subgroups of order 1, 2, 3, and 6
example : Fintype.card (ZMod 6) = 6 := by decide

-- ============================================================================
-- Section 4: Connection to finite fields
-- ============================================================================

-- The multiplicative group of ANY finite field is cyclic.
-- This is a deep theorem (proved in Galois.lean for specific cases).
--
-- For 𝔽₅: 𝔽₅ˣ ≅ ℤ/4ℤ (cyclic of order 4)
-- For 𝔽₃: 𝔽₃ˣ ≅ ℤ/2ℤ (cyclic of order 2)
-- For GF(9): GF(9)ˣ ≅ ℤ/8ℤ (cyclic of order 8)
--
-- In general: GF(q)ˣ ≅ ℤ/(q-1)ℤ