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 : FermatLastTheoremFor 3

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