Algebra & fields

GF(5): a prime field

Prove that arithmetic modulo 5 forms a field by checking every possible input.

-- GF(5): a prime field
-- History: Finite-field algebra · prime characteristic.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The multiplicative inverse of 2 is 3 in GF(5), because 2×3 leaves remainder 1.
-- Scope: Verifies the commutative ring laws and an inverse for each nonzero Fin 5 element. No general prime-modulus theorem or Mathlib Field instance is used.
-- Source: https://lean-lang.org/doc/api/Init/Data/Fin/Basic.html

abbrev F := Fin 5

example : ∀ a b c : F, (a+b)+c = a+(b+c) := by decide
example : ∀ a b : F, a+b = b+a := by decide
example : ∀ a : F, a+0 = a ∧ a+(-a) = 0 := by decide
example : ∀ a b c : F, (a*b)*c = a*(b*c) := by decide
example : ∀ a b : F, a*b = b*a := by decide
example : ∀ a : F, a*1 = a := by decide
example : ∀ a b c : F, a*(b+c) = a*b+a*c := by decide
example : (0 : F) ≠ 1 := by decide

-- This is the extra property that fails modulo 6.
theorem nonzero_inverse : ∀ a : F, a ≠ 0 → ∃ b : F, a*b = 1 := by
  decide

#eval (2 : F)*3

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Quantifying over Fin n checks every one of its finitely many values.

`Fin n`

Fin n contains the natural numbers less than n, each with a bound proof. Addition and multiplication wrap modulo n.

Background and proof scope

Finite-field algebra · prime characteristic

The multiplicative inverse of 2 is 3 in GF(5), because 2×3 leaves remainder 1.

Verifies the commutative ring laws and an inverse for each nonzero Fin 5 element. No general prime-modulus theorem or Mathlib Field instance is used.

Lean’s finite residue arithmetic

Expected output

Reference only. Run the file to check its actual result.

Exercise

Try Fin 7. Then try Fin 6 and see the inverse theorem fail.