Documentation

Mathlib.NumberTheory.FLT.Four

Fermat's Last Theorem for the case n = 4 #

There are no non-zero integers a, b and c such that a ^ 4 + b ^ 4 = c ^ 4.

def Fermat42 (a : ) (b : ) (c : ) :

Shorthand for three non-zero integers a, b, and c satisfying a ^ 4 + b ^ 4 = c ^ 2. We will show that no integers satisfy this equation. Clearly Fermat's Last theorem for n = 4 follows.

Equations
Instances For
    theorem Fermat42.comm {a : } {b : } {c : } :
    Fermat42 a b c Fermat42 b a c
    theorem Fermat42.mul {a : } {b : } {c : } {k : } (hk0 : k 0) :
    Fermat42 a b c Fermat42 (k * a) (k * b) (k ^ 2 * c)
    theorem Fermat42.ne_zero {a : } {b : } {c : } (h : Fermat42 a b c) :
    c 0
    def Fermat42.Minimal (a : ) (b : ) (c : ) :

    We say a solution to a ^ 4 + b ^ 4 = c ^ 2 is minimal if there is no other solution with a smaller c (in absolute value).

    Equations
    Instances For
      theorem Fermat42.exists_minimal {a : } {b : } {c : } (h : Fermat42 a b c) :
      ∃ (a0 : ) (b0 : ) (c0 : ), Fermat42.Minimal a0 b0 c0

      if we have a solution to a ^ 4 + b ^ 4 = c ^ 2 then there must be a minimal one.

      theorem Fermat42.coprime_of_minimal {a : } {b : } {c : } (h : Fermat42.Minimal a b c) :

      a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 must have a and b coprime.

      theorem Fermat42.minimal_comm {a : } {b : } {c : } :

      We can swap a and b in a minimal solution to a ^ 4 + b ^ 4 = c ^ 2.

      theorem Fermat42.neg_of_minimal {a : } {b : } {c : } :

      We can assume that a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 has positive c.

      theorem Fermat42.exists_odd_minimal {a : } {b : } {c : } (h : Fermat42 a b c) :
      ∃ (a0 : ) (b0 : ) (c0 : ), Fermat42.Minimal a0 b0 c0 a0 % 2 = 1

      We can assume that a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 has a odd.

      theorem Fermat42.exists_pos_odd_minimal {a : } {b : } {c : } (h : Fermat42 a b c) :
      ∃ (a0 : ) (b0 : ) (c0 : ), Fermat42.Minimal a0 b0 c0 a0 % 2 = 1 0 < c0

      We can assume that a minimal solution to a ^ 4 + b ^ 4 = c ^ 2 has a odd and c positive.

      theorem Int.coprime_of_sq_sum {r : } {s : } (h2 : IsCoprime s r) :
      IsCoprime (r ^ 2 + s ^ 2) r
      theorem Int.coprime_of_sq_sum' {r : } {s : } (h : IsCoprime r s) :
      IsCoprime (r ^ 2 + s ^ 2) (r * s)
      theorem Fermat42.not_minimal {a : } {b : } {c : } (h : Fermat42.Minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) :
      theorem not_fermat_42 {a : } {b : } {c : } (ha : a 0) (hb : b 0) :
      a ^ 4 + b ^ 4 c ^ 2

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

      To prove Fermat's Last Theorem, it suffices to prove it for odd prime exponents.