Fermat Last Theorem in the case n = 3

The goal of this file is to prove Fermat's Last Theorem in the case n = 3.

Main results

• fermatLastTheoremThree: Fermat's Last Theorem for n = 3: if a b c : ℕ are all non-zero then a ^ 3 + b ^ 3 ≠ c ^ 3.

Implementation details

We follow the proof in https://webusers.imj-prg.fr/~marc.hindry/Cours-arith.pdf, page 43.

The strategy is the following:

• The so called "Case 1", when 3 ∣ a * b * c is completely elementary and is proved using congruences modulo 9.
• To prove case 2, we consider the generalized equation a ^ 3 + b ^ 3 = u * c ^ 3, where a, b, and c are in the cyclotomic ring ℤ[ζ₃] (where ζ₃ is a primitive cube root of unity) and u is a unit of ℤ[ζ₃]. FermatLastTheoremForThree_of_FermatLastTheoremThreeGen (whose proof is rather elementary on paper) says that to prove Fermat's last theorem for exponent 3, it is enough to prove that this equation has no solutions such that c ≠ 0, ¬ λ ∣ a, ¬ λ ∣ b, λ ∣ c and IsCoprime a b (where we set λ := ζ₃ - 1). We call such a tuple a Solution'. A Solution is the same as a Solution' with the additional assumption that λ ^ 2 ∣ a + b. We then prove that, given S' : Solution', there is S : Solution such that the multiplicity of λ = ζ₃ - 1 in c is the same in S' and S (see exists_Solution_of_Solution'). In particular it is enough to prove that no Solution exists. The key point is a descent argument on the multiplicity of λ in c: starting with S : Solution we can find S₁ : Solution with multiplicity strictly smaller (see exists_Solution_multiplicity_lt) and this finishes the proof. To construct S₁ we go through a Solution' and then back to a Solution. More importantly, we cannot control the unit u, and this is the reason why we need to consider the generalized equation a ^ 3 + b ^ 3 = u * c ^ 3. The construction is completely explicit, but it depends crucially on IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent, a special case of Kummer's lemma.
• Note that we don't prove Case 1 for the generalized equation (in particular we don't prove that the generalized equation has no nontrivial solutions). This is because the proof, even if elementary on paper, would be quite annoying to formalize: indeed it involves a lot of explicit computations in ℤ[ζ₃] / (λ): this ring is isomorphic to ℤ / 9ℤ, but of course, even if we construct such an isomorphism, tactics like decide would not work.

theorem fermatLastTheoremThree_case_1 {a b c : ℤ} (hdvd : ¬3 ∣ a * b * c) : a ^ 3 + b ^ 3 ≠ c ^ 3

If a b c : ℤ are such that ¬ 3 ∣ a * b * c, then a ^ 3 + b ^ 3 ≠ c ^ 3.

theorem fermatLastTheoremThree_of_three_dvd_only_c (H : ∀ (a b c : ℤ), c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) : FermatLastTheoremFor 3

To prove Fermat's Last Theorem for n = 3, it is enough to show that for all a, b, c in ℤ such that c ≠ 0, ¬ 3 ∣ a, ¬ 3 ∣ b, a and b are coprime and 3 ∣ c, we have a ^ 3 + b ^ 3 ≠ c ^ 3.

def FermatLastTheoremForThreeGen {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) : Prop

FermatLastTheoremForThreeGen is the statement that a ^ 3 + b ^ 3 = u * c ^ 3 has no nontrivial solutions in 𝓞 K for all u : (𝓞 K)ˣ such that ¬ λ ∣ a, ¬ λ ∣ b and λ ∣ c. The reason to consider FermatLastTheoremForThreeGen is to make a descent argument working.

theorem FermatLastTheoremForThree_of_FermatLastTheoremThreeGen {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : FermatLastTheoremForThreeGen hζ → FermatLastTheoremFor 3

To prove FermatLastTheoremFor 3, it is enough to prove FermatLastTheoremForThreeGen.

structure FermatLastTheoremForThreeGen.Solution' {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) : Type u_1

Solution' is a tuple given by a solution to a ^ 3 + b ^ 3 = u * c ^ 3, where a, b, c and u are as in FermatLastTheoremForThreeGen. See Solution for the actual structure on which we will do the descent.

• a : NumberField.RingOfIntegers K
• b : NumberField.RingOfIntegers K
• c : NumberField.RingOfIntegers K
• u : (NumberField.RingOfIntegers K)ˣ
• ha : ¬hζ.toInteger - 1 ∣ self.a
• hb : ¬hζ.toInteger - 1 ∣ self.b
• hc : self.c ≠ 0
• coprime : IsCoprime self.a self.b
• hcdvd : hζ.toInteger - 1 ∣ self.c
• H : self.a ^ 3 + self.b ^ 3 = ↑self.u * self.c ^ 3

structure FermatLastTheoremForThreeGen.Solution {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) extends FermatLastTheoremForThreeGen.Solution' hζ : Type u_1

Solution is the same as Solution' with the additional assumption that λ ^ 2 ∣ a + b.

• a : NumberField.RingOfIntegers K
• b : NumberField.RingOfIntegers K
• c : NumberField.RingOfIntegers K
• u : (NumberField.RingOfIntegers K)ˣ
• ha : ¬hζ.toInteger - 1 ∣ self.a
• hb : ¬hζ.toInteger - 1 ∣ self.b
• hc : self.c ≠ 0
• coprime : IsCoprime self.a self.b
• hcdvd : hζ.toInteger - 1 ∣ self.c
• H : self.a ^ 3 + self.b ^ 3 = ↑self.u * self.c ^ 3
• hab : (hζ.toInteger - 1) ^ 2 ∣ self.a + self.b

theorem FermatLastTheoremForThreeGen.Solution'.multiplicity_lambda_c_finite {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : FiniteMultiplicity (hζ.toInteger - 1) S'.c

For any S' : Solution', the multiplicity of λ in S'.c is finite.

noncomputable def FermatLastTheoremForThreeGen.Solution'.multiplicity {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) : ℕ

Given S' : Solution', S'.multiplicity is the multiplicity of λ in S'.c, as a natural number.

noncomputable def FermatLastTheoremForThreeGen.Solution.multiplicity {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) : ℕ

Given S : Solution, S.multiplicity is the multiplicity of λ in S.c, as a natural number.

def FermatLastTheoremForThreeGen.Solution.isMinimal {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) : Prop

We say that S : Solution is minimal if for all S₁ : Solution, the multiplicity of λ in S.c is less or equal than the multiplicity in S₁.c.

theorem FermatLastTheoremForThreeGen.Solution.exists_minimal {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) : ∃ (S₁ : Solution hζ), S₁.isMinimal

If there is a solution then there is a minimal one.

theorem FermatLastTheoremForThreeGen.a_cube_b_cube_congr_one_or_neg_one {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : (hζ.toInteger - 1) ^ 4 ∣ S'.a ^ 3 - 1 ∧ (hζ.toInteger - 1) ^ 4 ∣ S'.b ^ 3 + 1 ∨ (hζ.toInteger - 1) ^ 4 ∣ S'.a ^ 3 + 1 ∧ (hζ.toInteger - 1) ^ 4 ∣ S'.b ^ 3 - 1

Given S' : Solution', then S'.a and S'.b are both congruent to 1 modulo λ ^ 4 or are both congruent to -1.

theorem FermatLastTheoremForThreeGen.lambda_pow_four_dvd_c_cube {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : (hζ.toInteger - 1) ^ 4 ∣ S'.c ^ 3

Given S' : Solution', we have that λ ^ 4 divides S'.c ^ 3.

theorem FermatLastTheoremForThreeGen.lambda_sq_dvd_c {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : (hζ.toInteger - 1) ^ 2 ∣ S'.c

Given S' : Solution', we have that λ ^ 2 divides S'.c.

theorem FermatLastTheoremForThreeGen.Solution'.two_le_multiplicity {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : 2 ≤ S'.multiplicity

Given S' : Solution', we have that 2 ≤ S'.multiplicity.

theorem FermatLastTheoremForThreeGen.Solution.two_le_multiplicity {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : 2 ≤ S.multiplicity

Given S : Solution, we have that 2 ≤ S.multiplicity.

theorem FermatLastTheoremForThreeGen.a_cube_add_b_cube_eq_mul {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) : S'.a ^ 3 + S'.b ^ 3 = (S'.a + S'.b) * (S'.a + ↑⋯.unit * S'.b) * (S'.a + ↑⋯.unit ^ 2 * S'.b)

Given S' : Solution', the key factorization of S'.a ^ 3 + S'.b ^ 3.

theorem FermatLastTheoremForThreeGen.lambda_sq_dvd_or_dvd_or_dvd {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : (hζ.toInteger - 1) ^ 2 ∣ S'.a + S'.b ∨ (hζ.toInteger - 1) ^ 2 ∣ S'.a + ↑⋯.unit * S'.b ∨ (hζ.toInteger - 1) ^ 2 ∣ S'.a + ↑⋯.unit ^ 2 * S'.b

Given S' : Solution', we have that λ ^ 2 divides one amongst S'.a + S'.b, S'.a + η * S'.b and S'.a + η ^ 2 * S'.b.

theorem FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : ∃ (a' : NumberField.RingOfIntegers K) (b' : NumberField.RingOfIntegers K), a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧ IsCoprime a' b' ∧ ¬hζ.toInteger - 1 ∣ a' ∧ ¬hζ.toInteger - 1 ∣ b' ∧ (hζ.toInteger - 1) ^ 2 ∣ a' + b'

Given S' : Solution', we may assume that λ ^ 2 divides S'.a + S'.b ∨ λ ^ 2 (see also the result below).

theorem FermatLastTheoremForThreeGen.exists_Solution_of_Solution' {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : Solution' hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : ∃ (S₁ : Solution hζ), S₁.multiplicity = S'.multiplicity

Given S' : Solution', then there is S₁ : Solution such that S₁.multiplicity = S'.multiplicity.

theorem FermatLastTheoremForThreeGen.Solution.a_add_eta_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) : S.a + ↑⋯.unit * S.b = S.a + S.b + (hζ.toInteger - 1) * S.b

theorem FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) : hζ.toInteger - 1 ∣ S.a + ↑⋯.unit * S.b

Given (S : Solution), we have that λ ∣ (S.a + η * S.b).

theorem FermatLastTheoremForThreeGen.Solution.lambda_dvd_a_add_eta_sq_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) : hζ.toInteger - 1 ∣ S.a + ↑⋯.unit ^ 2 * S.b

Given (S : Solution), we have that λ ∣ (S.a + η ^ 2 * S.b).

theorem FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : ¬(hζ.toInteger - 1) ^ 2 ∣ S.a + ↑⋯.unit * S.b

Given (S : Solution), we have that λ ^ 2 does not divide S.a + η * S.b.

theorem FermatLastTheoremForThreeGen.Solution.lambda_sq_not_dvd_a_add_eta_sq_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : ¬(hζ.toInteger - 1) ^ 2 ∣ S.a + ↑⋯.unit ^ 2 * S.b

Given (S : Solution), we have that λ ^ 2 does not divide S.a + η ^ 2 * S.b.

theorem FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_b_of_dvd_a_add_eta_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] {p : NumberField.RingOfIntegers K} (hp : Prime p) (hpab : p ∣ S.a + S.b) (hpaηb : p ∣ S.a + ↑⋯.unit * S.b) : Associated p (hζ.toInteger - 1)

If p : 𝓞 K is a prime that divides both S.a + S.b and S.a + η * S.b, then p is associated with λ.

theorem FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_b_of_dvd_a_add_eta_sq_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] {p : NumberField.RingOfIntegers K} (hp : Prime p) (hpab : p ∣ S.a + S.b) (hpaηsqb : p ∣ S.a + ↑⋯.unit ^ 2 * S.b) : Associated p (hζ.toInteger - 1)

If p : 𝓞 K is a prime that divides both S.a + S.b and S.a + η ^ 2 * S.b, then p is associated with λ.

theorem FermatLastTheoremForThreeGen.Solution.associated_of_dvd_a_add_eta_mul_b_of_dvd_a_add_eta_sq_mul_b {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] {p : NumberField.RingOfIntegers K} (hp : Prime p) (hpaηb : p ∣ S.a + ↑⋯.unit * S.b) (hpaηsqb : p ∣ S.a + ↑⋯.unit ^ 2 * S.b) : Associated p (hζ.toInteger - 1)

If p : 𝓞 K is a prime that divides both S.a + η * S.b and S.a + η ^ 2 * S.b, then p is associated with λ.

noncomputable def FermatLastTheoremForThreeGen.Solution.Solution'_descent {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : Solution' hζ

Given S : Solution, we construct S₁ : Solution', with smaller multiplicity of λ in c (see Solution'_descent_multiplicity_lt below.).

theorem FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : S.Solution'_descent.multiplicity = S.multiplicity - 1

We have that S.Solution'_descent.multiplicity = S.multiplicity - 1.

theorem FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity_lt {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : S.Solution'_descent.multiplicity < S.multiplicity

We have that S.Solution'_descent.multiplicity < S.multiplicity.

theorem FermatLastTheoremForThreeGen.Solution.exists_Solution_multiplicity_lt {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : Solution hζ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : ∃ (S₁ : Solution hζ), S₁.multiplicity < S.multiplicity

Given any S : Solution, there is another S₁ : Solution such that S₁.multiplicity < S.multiplicity

theorem fermatLastTheoremThree : FermatLastTheoremFor 3

Fermat's Last Theorem for n = 3: if a b c : ℕ are all non-zero then a ^ 3 + b ^ 3 ≠ c ^ 3.