HepLean Documentation

Mathlib.NumberTheory.FLT.Three

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 #

Implementation details #

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

The strategy is the following:

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 b3 cIsCoprime a ba ^ 3 + b ^ 3 c ^ 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) :

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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    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.

    Instances For
      theorem FermatLastTheoremForThreeGen.Solution'.ha {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (self : FermatLastTheoremForThreeGen.Solution' ) :
      ¬.toInteger - 1 self.a
      theorem FermatLastTheoremForThreeGen.Solution'.hb {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (self : FermatLastTheoremForThreeGen.Solution' ) :
      ¬.toInteger - 1 self.b
      theorem FermatLastTheoremForThreeGen.Solution'.hc {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (self : FermatLastTheoremForThreeGen.Solution' ) :
      self.c 0
      theorem FermatLastTheoremForThreeGen.Solution'.hcdvd {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (self : FermatLastTheoremForThreeGen.Solution' ) :
      .toInteger - 1 self.c
      theorem FermatLastTheoremForThreeGen.Solution'.H {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (self : FermatLastTheoremForThreeGen.Solution' ) :
      self.a ^ 3 + self.b ^ 3 = self.u * self.c ^ 3

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

      Instances For
        theorem FermatLastTheoremForThreeGen.Solution.hab {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (self : FermatLastTheoremForThreeGen.Solution ) :
        (.toInteger - 1) ^ 2 self.a + self.b

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

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

        Equations
        Instances For

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

          Equations
          • S.multiplicity = S.multiplicity
          Instances For

            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.

            Equations
            Instances For

              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' : FermatLastTheoremForThreeGen.Solution' ) [NumberField K] [IsCyclotomicExtension {3} K] :
              (.toInteger - 1) ^ 4 S'.a ^ 3 - 1 (.toInteger - 1) ^ 4 S'.b ^ 3 + 1 (.toInteger - 1) ^ 4 S'.a ^ 3 + 1 (.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' : FermatLastTheoremForThreeGen.Solution' ) [NumberField K] [IsCyclotomicExtension {3} K] :
              (.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' : FermatLastTheoremForThreeGen.Solution' ) [NumberField K] [IsCyclotomicExtension {3} K] :
              (.toInteger - 1) ^ 2 S'.c

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

              Given S' : Solution', we have that 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' : FermatLastTheoremForThreeGen.Solution' ) :
              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' : FermatLastTheoremForThreeGen.Solution' ) [NumberField K] [IsCyclotomicExtension {3} K] [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a b] :
              (.toInteger - 1) ^ 2 S'.a + S'.b (.toInteger - 1) ^ 2 S'.a + .unit * S'.b (.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' : FermatLastTheoremForThreeGen.Solution' ) [NumberField K] [IsCyclotomicExtension {3} K] [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a b] :
              ∃ (a' : NumberField.RingOfIntegers K) (b' : NumberField.RingOfIntegers K), a' ^ 3 + b' ^ 3 = S'.u * S'.c ^ 3 IsCoprime a' b' ¬.toInteger - 1 a' ¬.toInteger - 1 b' (.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' : FermatLastTheoremForThreeGen.Solution' ) [NumberField K] [IsCyclotomicExtension {3} K] [DecidableRel fun (a b : NumberField.RingOfIntegers K) => a b] :
              ∃ (S₁ : FermatLastTheoremForThreeGen.Solution ), 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 : FermatLastTheoremForThreeGen.Solution ) :
              S.a + .unit * S.b = S.a + S.b + (.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 : FermatLastTheoremForThreeGen.Solution ) :
              .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 : FermatLastTheoremForThreeGen.Solution ) :
              .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 : FermatLastTheoremForThreeGen.Solution ) [NumberField K] [IsCyclotomicExtension {3} K] :
              ¬(.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 : FermatLastTheoremForThreeGen.Solution ) [NumberField K] [IsCyclotomicExtension {3} K] :
              ¬(.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 : FermatLastTheoremForThreeGen.Solution ) [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 (.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 : FermatLastTheoremForThreeGen.Solution ) [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 (.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 : FermatLastTheoremForThreeGen.Solution ) [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 (.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 λ.

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity {K : Type u_1} [Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution ) [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 : FermatLastTheoremForThreeGen.Solution ) [NumberField K] [IsCyclotomicExtension {3} K] :
                S.Solution'_descent.multiplicity < S.multiplicity

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

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

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