# Statement of Fermat's Last Theorem #

This file states Fermat's Last Theorem. We provide a statement over a general semiring with specific exponent, along with the usual statement over the naturals.

def FermatLastTheoremWith (α : Type u_1) [] (n : ) :

Statement of Fermat's Last Theorem over a given semiring with a specific exponent.

Equations
Instances For

Statement of Fermat's Last Theorem over the naturals for a given exponent.

Equations
Instances For

Statement of Fermat's Last Theorem: a ^ n + b ^ n = c ^ n has no nontrivial natural solution when n ≥ 3.

Equations
Instances For
theorem FermatLastTheoremWith.mono {α : Type u_1} [] [] {m : } {n : } (hmn : m n) (hm : ) :
theorem FermatLastTheoremFor.mono {m : } {n : } (hmn : m n) (hm : ) :
theorem fermatLastTheoremWith_of_fermatLastTheoremWith_coprime {n : } {R : Type u_2} [] [] [] (hn : ∀ (a b c : R), a 0b 0c 0{a, b, c}.gcd id = 1a ^ n + b ^ n c ^ n) :

To prove Fermat Last Theorem in any semiring that is a NormalizedGCDMonoid one can assume that the gcd of {a, b, c} is 1.

theorem dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT {n : } {p : } (hp : ) {a : } {b : } {c : } (hpa : p a) (hpb : p b) (HF : a ^ n + b ^ n + c ^ n = 0) :
p c
theorem isCoprime_of_gcd_eq_one_of_FLT {n : } {a : } {b : } {c : } (Hgcd : {a, b, c}.gcd id = 1) (HF : a ^ n + b ^ n + c ^ n = 0) :