mathlib documentation

number_theory.fermat4

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.

source
def fermat_42 (a b c : ℤ) :
Prop

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
source
theorem fermat_42.comm {a b c : ℤ} :
fermat_42 a b c ↔ fermat_42 b a c
source
theorem fermat_42.mul {a b c k : ℤ} (hk0 : k ≠ 0) :
fermat_42 a b c ↔ fermat_42 (k * a) (k * b) (k ^ 2 * c)
source
theorem fermat_42.ne_zero {a b c : ℤ} (h : fermat_42 a b c) :
c ≠ 0
source
def fermat_42.minimal (a b c : ℤ) :
Prop

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
source
theorem fermat_42.exists_minimal {a b c : ℤ} (h : fermat_42 a b c) :
∃ (a0 b0 c0 : ℤ), fermat_42.minimal a0 b0 c0

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

source
theorem fermat_42.coprime_of_minimal {a b c : ℤ} (h : fermat_42.minimal a b c) :
is_coprime a b

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

source
theorem fermat_42.minimal_comm {a b c : ℤ} :
fermat_42.minimal a b c → fermat_42.minimal b a c

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

source
theorem fermat_42.neg_of_minimal {a b c : ℤ} :
fermat_42.minimal a b c → fermat_42.minimal a b (-c)

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

source
theorem fermat_42.exists_odd_minimal {a b c : ℤ} (h : fermat_42 a b c) :
∃ (a0 b0 c0 : ℤ), fermat_42.minimal a0 b0 c0 ∧ a0 % 2 = 1

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

source
theorem fermat_42.exists_pos_odd_minimal {a b c : ℤ} (h : fermat_42 a b c) :
∃ (a0 b0 c0 : ℤ), fermat_42.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.

source
theorem int.coprime_of_sq_sum {r s : ℤ} (h2 : is_coprime s r) :
is_coprime (r ^ 2 + s ^ 2) r
source
theorem int.coprime_of_sq_sum' {r s : ℤ} (h : is_coprime r s) :
is_coprime (r ^ 2 + s ^ 2) (r * s)
source
theorem fermat_42.not_minimal {a b c : ℤ} (h : fermat_42.minimal a b c) (ha2 : a % 2 = 1) (hc : 0 < c) :
false
source
theorem not_fermat_42 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
a ^ 4 + b ^ 4 ≠ c ^ 2
source
theorem not_fermat_4 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
a ^ 4 + b ^ 4 ≠ c ^ 4