Fermat’s Last Theorem for Exponent 3

1 Preliminaries

This chapter provides the necessary prerequisites used throughout this project. We begin by introducing the notation that will be employed, followed by essential definitions and preliminary results required for formalising our arguments.

1.1 Notation

In this section, we define the notation and symbols that will be consistently used in this work.

Symbol

Description

\(:=\)

Definition

\(\forall \)

Universal quantification

\(\exists \)

Existential quantification

\(\exists !\)

Unique existential quantification

\(\mathbb {N}\)

Set of natural numbers

\(\mathbb {Z}\)

Set of integer numbers

\(\mathbb {Z}_n\)

Set of integers modulo \(n\)

\(\mathbb {Q}\)

Set of rational numbers

\(X/Y\)

Field extension

\([Y:X]\)

Degree of field extension

\(\times \)

Cartesian product

\([n]\)

Equivalence class of \(n\)

\(\mid \)

Divisibility relation

\(\nmid \)

Negation of divisibility relation

\(\gcd \)

Greatest common divisor

\(\zeta _n\)

Primitive \(n\)-th root of unity


1.2 Definitions

In this section, each definition is articulated as clearly as possible to maximise clarity and precision.

Definition 1.1 Monoid
#

Let \(X\) be a non-empty set.
Let \(\circ : X\times X \to X\) be an internal composition law on \(X\).

A monoid is a pair \(\mathcal{M}:= (X, \circ )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x\circ y)\circ z= x\circ (y\circ z) = x\circ y \circ z\)

  2. \(\exists e \in X : \forall x \in X,\ x\circ e = e \circ x = x\)

Definition 1.2 Commutative Monoid
#

Let \(X\) be a non-empty set.
Let \(\circ : X\times X \to X\) be an internal composition law on \(X\).

A commutative monoid is a pair \(\mathcal{M}_c:= (X, \circ )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x\circ y)\circ z= x\circ (y\circ z) = x\circ y \circ z\)

  2. \(\exists e \in X : \forall x \in X,\ x\circ e = e \circ x = x\)

  3. \(\forall x,y\in X,\ x\circ y = y\circ x\)

Definition 1.3 GCD Monoid
#

Let \(X\) be a non-empty set.
Let \(\circ : X\times X \to X\) be an internal composition law on \(X\).

A gcd monoid is a pair \(\mathcal{M}_{\gcd }:= (X, \circ )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x\circ y)\circ z= x\circ (y\circ z) = x\circ y \circ z\)

  2. \(\exists e \in X : \forall x \in X,\ x\circ e = e \circ x = x\)

  3. \(\forall x,y\in X,\ x\circ y = y\circ x\)

  4. \(\forall x,y\in X,\ \exists d \in X : (d\mid x) \land (d\mid y) \land \left(\forall c \in X,\ c\mid x \land c\mid y \Rightarrow c\mid d\right)\)

Definition 1.4 Group
#

Let \(X\) be a non-empty set.
Let \(\circ : X\times X \to X\) be an internal composition law on \(X\).

A group is a pair \(\mathcal{G}:= (X, \circ )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x\circ y)\circ z= x\circ (y\circ z) = x\circ y \circ z\)

  2. \(\exists e \in X : \forall x \in X,\ x\circ e = e \circ x = x\)

  3. \(\forall x \in X,\ \exists x'\in X: x\circ x' = x'\circ x = e\)

Definition 1.5 Commutative Group
#

Let \(X\) be a non-empty set.
Let \(\circ : X\times X \to X\) be an internal composition law on \(X\).

A commutative group is a pair \(\mathcal{G}_c:= (X, \circ )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x\circ y)\circ z= x\circ (y\circ z) = x\circ y \circ z\)

  2. \(\exists e \in X : \forall x \in X,\ x\circ e = e \circ x = x\)

  3. \(\forall x \in X,\ \exists x'\in X: x\circ x' = x'\circ x = e\)

  4. \(\forall x,y\in X,\ x\circ y = y\circ x\)

Definition 1.6 Semiring
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A semiring is a triple \(\mathcal{S}:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  5. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  6. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  7. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

Definition 1.7 Commutative Semiring
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A commutative semiring is a triple \(\mathcal{S}_c:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  5. \(\forall x,y\in X,\ x\cdot y = y\cdot x\)

  6. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  7. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  8. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

Definition 1.8 Ring
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A ring is a triple \(\mathcal{R}:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x \in X,\ \exists (-x)\in X: x+(-x) = (-x)+x = 0\)

  5. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  6. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  7. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  8. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

Definition 1.9 Commutative Ring
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A commutative ring is a triple \(\mathcal{R}_c:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x \in X,\ \exists (-x)\in X: x+(-x) = (-x)+x = 0\)

  5. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  6. \(\forall x,y\in X,\ x\cdot y = y\cdot x\)

  7. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  8. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  9. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

Definition 1.10 Left Ideal
#

Let \((X, +, \cdot )\) be a ring.

A left ideal is a subset \(I \subseteq X\) satisfying:

  1. \((I, +)\) is a subgroup of \((X, +)\)

  2. \(\forall i\in I,\ \forall x\in X,\ x\cdot i\in I\)

Definition 1.11 Right Ideal
#

Let \((X, +, \cdot )\) be a ring.

A right ideal is a subset \(I \subseteq X\) satisfying:

  1. \((I, +)\) is a subgroup of \((X, +)\)

  2. \(\forall i\in I,\ \forall x\in X,\ i\cdot x\in I\)

Definition 1.12 Ideal
#

Let \((X, +, \cdot )\) be a ring.

An ideal or two-sided ideal is a subset \(I \subseteq X\) satisfying:

  1. \((I, +)\) is a subgroup of \((X, +)\)

  2. \(\forall i\in I,\ \forall x\in X,\ x\cdot i\in I\)

  3. \(\forall i\in I,\ \forall x\in X,\ i\cdot x\in I\)

Definition 1.13 Domain
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A domain is a triple \(\mathcal{D}:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x \in X,\ \exists (-x)\in X: x+(-x) = (-x)+x = 0\)

  5. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  6. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  7. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  8. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

  9. \(\forall x,y \in X,\ x\cdot y = 0 \Rightarrow x=0 \lor y=0\)

Definition 1.14 Commutative Domain
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A commutative or integral domain is a triple \(\mathcal{D}_c:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x \in X,\ \exists (-x)\in X: x+(-x) = (-x)+x = 0\)

  5. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  6. \(\forall x,y\in X,\ x\cdot y = y\cdot x\)

  7. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  8. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  9. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

  10. \(\forall x,y \in X,\ x\cdot y = 0 \Rightarrow x=0 \lor y=0\)

Definition 1.15 Field
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A field is a triple \(\mathbb {F}:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x \in X,\ \exists (-x)\in X: x+(-x) = (-x)+x = 0\)

  5. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  6. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  7. \(\forall x \in X,\ \exists x^{-1}\in X: x\cdot x^{-1} = x^{-1}\cdot x = 1\)

  8. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  9. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

Definition 1.16 Commutative Field
#

Let \(X\) be a non-empty set.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : X\times X \to X\) be a multiplicative internal composition law on \(X\).

A commutative field is a triple \(\mathbb {F}_c:= (X, +, \cdot )\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x \in X,\ \exists (-x)\in X: x+(-x) = (-x)+x = 0\)

  5. \(\forall x,y,z\in X,\ (x\cdot y)\cdot z= x\cdot (y\cdot z) = x\cdot y\cdot z\)

  6. \(\forall x,y\in X,\ x\cdot y = y\cdot x\)

  7. \(\exists 1 \in X : \forall x \in X,\ x\cdot 1 = 1\cdot x = x\)

  8. \(\forall x \in X,\ \exists x^{-1}\in X: x\cdot x^{-1} = x^{-1}\cdot x = 1\)

  9. \(\forall x,y,z \in X,\ x\cdot (y+z)=x\cdot y+x\cdot z\)

  10. \(\forall x,y,z \in X,\ (x+y)\cdot z=x\cdot z+y\cdot z\)

Definition 1.17 Fundamental System of Field
#

Let \((X, +, \cdot )\) be a field endowed with a topology \(\mathcal{T}\).
Let \(I \subseteq \mathbb {N}\) be an index set.

A fundamental system of \(X\) is a collection \( \mathcal{U} = \{ U_i \} _{i \in I} \) of open sets in \( X \) such that:

  1. \(\forall i \in I,\ 0 \in U_i\).

  2. \(\forall V \ni 0,\ \exists i \in I : U_i \subseteq V\).

Definition 1.18 Vector Space
#

Let \(X\) be a non-empty set.
Let \((\mathbb {K},+,\cdot )\) be a field.
Let \(+: X\times X \to X\) be an additive internal composition law on \(X\).
Let \(\cdot : \mathbb {K}\times X \to X\) be a multiplicative external composition law on \(X\).

A \(\mathbb {K}\)-vector space or \(\mathbb {K}\)-linear space is a triple \(\mathcal{V}:= (X, +, \cdot )_{\mathbb {K}}\) satisfying:

  1. \(\forall x,y,z\in X,\ (x+y)+z= x+(y+z) = x+y+z\)

  2. \(\forall x,y\in X,\ x+y = y+x\)

  3. \(\exists 0 \in X : \forall x \in X,\ x+0 = 0+x = x\)

  4. \(\forall x \in X,\ \exists (-x)\in X: x+(-x) = (-x)+x = 0\)

  5. \(\forall x \in X,\ \forall k,\ell \in \mathbb {K},\ k\cdot _X(\ell \cdot _X x)= (k\cdot _{\mathbb {K}}\ell )\cdot _X x\)

  6. \(\exists 1 \in \mathbb {K}: \forall x \in X,\ 1\cdot x = x\)

  7. \(\forall x,y \in X,\ \forall k\in \mathbb {K},\ k\cdot (x+_Xy)=k\cdot x+_Xk\cdot y\)

  8. \(\forall k,\ell \in \mathbb {K},\ \forall x\in X,\ (k+_\mathbb {K}\ell )\cdot x=k\cdot x+_X\ell \cdot x\)

From now on, we shall employ the notation \(X\) in place of the more explicit \((X, +, \cdot )\) to denote a field, commutative ring, domain, or similar algebraic structures when the context unambiguously implies the operations involved.

Definition 1.19 Field Extension
#

Let \((X, +, \cdot )\) be a field.
Let \((Y, +, \cdot )\) be a field such that \(Y \subseteq X\).

A field extension is the pair \(X/Y\) such that the operations of \(Y\) are those of \(X\) restricted to \(Y\).

Definition 1.20 Degree of Field Extension
#

Let \((X, +, \cdot )\) be a field.
Let \((Y, +, \cdot )\) be a field such that \(Y \subseteq X\).
Let \(X/Y\) be a field extension.

The degree of \(X/Y\), denoted as \([Y:X]\), is the dimension of \(X\) as a vector space over \(Y\).

Definition 1.21 Algebraic Field Extension
#

Let \((X, +, \cdot )\) be a field.
Let \((Y, +, \cdot )\) be a field such that \(Y \subseteq X\).

An algebraic field extension is the field extension \(X/Y\) such that its degree \([Y:X]\) is finite.

Definition 1.22 Extension Field
#

Let \((X, +, \cdot )\) be a field.
Let \((Y, +, \cdot )\) be a field such that \(Y \subseteq X\).
Let \(X/Y\) be a field extension.

The field \(X\) is said to be an extension field of \(Y\).

Definition 1.23 Subfield
#

Let \((X, +, \cdot )\) be a field.
Let \((Y, +, \cdot )\) be a field such that \(Y \subseteq X\).
Let \(X/Y\) be a field extension.

The field \(Y\) is said to be a subfield of \(X\).

Definition 1.24 Number Field
#

Let \((X, +, \cdot )\) be a field.
Let \((\mathbb {Q}, +, \cdot )\) be the field of rational numbers such that \(\mathbb {Q}\subseteq X\).
Let \(X/\mathbb {Q}\) be an algebraic field extension.

The extension field \(X\) is said to be a number field or an algebraic number field.

Definition 1.25 Root of Unity
#

Let \(n \in \mathbb {N}_{+}\).

A \(n\)-th root of unity is an element \(\zeta \in \mathbb {C}\) such that \(\zeta ^n = 1\).

Definition 1.26 Primitive Root of Unity
#

Let \(n \in \mathbb {N}_{+}\).

A primitive \(n\)-th root of unity is an element \(\zeta \in \mathbb {C}\) satisfying:

  1. \(\zeta ^n = 1\).

  2. \(\forall k \in \mathbb {N}_{+},\ k {\lt} n \implies \zeta ^k \neq 1\).

Definition 1.27 Cyclotomic Polynomial
#

Let \(n \in \mathbb {N}_{+}\).
Let \(\zeta \in \mathbb {C}\) be a primitive \(n\)-th root of unity.

The \(n\)-th cyclotomic polynomial is the unique monic polynomial with integer coefficients whose roots are the primitive \(n\)-th roots of unity:

\[ \Phi _n(x) = \prod _{\substack {1 \leq k \leq n \\ \gcd (k, n) = 1}} \left( x - \zeta ^k \right) \]
Definition 1.28 Cyclotomic Extension Field
#

Let \(n \in \mathbb {N}_{+}\).
Let \(\zeta _n \in \mathbb {C}\) be a primitive \(n\)-th root of unity.
Let \(X\) be a field.

The \(n\)-th cyclotomic extension field or \(n\)-th cyclotomic field is a field \(X(\zeta _n)\) obtained by adjoining \(\zeta _n\) to \(X\).


1.3 Results

In this section, we state some preliminary results that are crucial for the development of our formal proofs.

Theorem 1.29
✓
#

Lean declarations

Let \(p \in \mathbb {N}\) be prime.

If \(\zeta _p\) is a primitive \(p\)-th root of unity, then \(\zeta _p - 1\) is prime.

Proof ▶

This has already been formalised and included in Mathlib.

Lemma 1.30
✓
#

Lean declarations

Let \(R\) be a commutative semiring, domain and normalised \(\gcd \) monoid.
Let \(a, b, c \in R\).
Let \(n \in \mathbb {N}\).

Then, to prove Fermat’s Last Theorem for exponent \(n\) in \(R\), one can assume, without loss of generality, that \(\gcd (a,b,c)=1\).

Proof ▶

This has already been formalised and included in Mathlib.

Lemma 1.31
✓
#

Lean declarations

Let \(\mathbb {Z}_9\) be the ring of integers modulo \(9\).
Let \(\mathbb {Z}_3\) be the ring of integers modulo \(3\).
Let \(n \in \mathbb {Z}_9\).
Let \(\phi : \mathbb {Z}_9 \to \mathbb {Z}_3\) be the canonical ring homomorphism.
Let \(\phi (n) \neq 0\).

Then \(n^3=1 \lor n^3=8\).

Proof ▶

This has already been formalised and included in Mathlib.