def primes_and_inverses : List ℤ

Equations

• primes_and_inverses = (List.map (fun (p : ℤ) => [p, -p]) do let a ← List.filter (fun (b : ℕ) => decide (Nat.Prime b)) (List.range 100) pure ↑a).join

def cayley_table (n : ℕ) : List (List ℤ)

Equations

• One or more equations did not get rendered due to their size.

def T : List (List ℤ)

Equations

• T = cayley_table 30

def sub_array (T : List (List ℤ)) (r : ℕ) (c : ℕ) (v : ℕ) (w : ℕ) : List (List ℤ)

Equations

• sub_array T r c v w = List.map (fun (row : List ℤ) => List.take w (List.drop c row)) (List.take v (List.drop r T))

def TT1 : List (List ℤ)

Equations

• TT1 = sub_array T 1 1 3 3

structure Beta : Type

• A : ℤ
• B : ℤ
• L : ℤ
• E : ℤ

def create_beta (TTi : List (List ℤ)) : Beta

Equations

• create_beta TTi = { A := TTi.head!.head!, B := TTi.head!.getLast!, L := TTi.getLast!.head!, E := TTi.getLast!.getLast! }

def β1 : Beta

Equations

• β1 = create_beta TT1

theorem lemma_4_1 (m : ℤ) (n : ℤ) (c : ℤ) (k : ℤ) : let TTi_A := m + n; let TTi_B := m + (n + k); let TTi_L := m + c + n; let TTi_E := m + c + (n + k); TTi_B + TTi_L = TTi_A + TTi_E

theorem lemma_4_2 (p : ℕ) (hp : Nat.Prime p) (h : p > 3) : ∃ (n : ℕ), p = 6 * n + 1 ∨ p = 6 * n - 1