Fermat's Last Theorem

There are many ways of stating Fermat's Last Theorem. In this file, we give the traditional statement using the positive integers ℕ+, and deduce it from a proof of Mathlib's version FermatLastTheorem of the statement (which is a statement about the nonnegative integers ℕ.)

Note that many of the files imported by this file contain "sorried" theorems, that is, theorems whose proofs are not yet complete. So whilst the below looks like a complete proof of Fermat's Last Theorem, it currently relies on many incomplete proofs along the way, and is likely to do so for several years.

theorem PNat.pow_add_pow_ne_pow (x : ℕ+) (y : ℕ+) (z : ℕ+) (n : ℕ) (hn : n > 2) : x ^ n + y ^ n ≠ z ^ n

Fermat's Last Theorem for positive naturals.